Finiteness of UpWords given finite alphabet

set.mm

@@ -38330,6 +38330,16 @@ technically classes despite morally (and provably) being sets, like ` 1 `
       ( crab cv wcel wa cab df-rab ssab2 eqsstri ) ABCDBECFAGBHCABCIABCJK $.
   $}
 
+  ${
+    $d x A $.  $d x B $.  $d x ph $.
+    rabss3d.1 $e |- ( ( ph /\ ( x e. A /\ ps ) ) -> x e. B ) $.
+    $( Subclass law for restricted abstraction.  (Contributed by Thierry
+       Arnoux, 25-Sep-2017.) $)
+    rabss3d $p |- ( ph -> { x e. A | ps } C_ { x e. B | ps } ) $=
+      ( crab nfv nfrab1 cv wcel wa simprr jca ex rabid 3imtr4g ssrd ) ACBCDGZBC
+      EGZACHBCDIBCEIACJZDKZBLZUAEKZBLZUASKUATKAUCUEAUCLUDBFAUBBMNOBCDPBCEPQR $.
+  $}
+
   ${
     $d A x $.
     ssrab3.1 $e |- B = { x e. A | ph } $.
@@ -472279,16 +472289,6 @@ Class abstractions (a.k.a. class builders)
     ( csn wss wcel c0 wceq wo sssn snnzg neneqd pm2.21d sneqrg jaod imp sylan2b
     ) ADZBDZEACFZRGHZRSHZIZABHZRBJTUCUDTUAUDUBTUAUDTRGACKLMABCNOPQ $.
 
-  ${
-    $d x A $.  $d x B $.  $d x ph $.
-    rabss3d.1 $e |- ( ( ph /\ ( x e. A /\ ps ) ) -> x e. B ) $.
-    $( Subclass law for restricted abstraction.  (Contributed by Thierry
-       Arnoux, 25-Sep-2017.) $)
-    rabss3d $p |- ( ph -> { x e. A | ps } C_ { x e. B | ps } ) $=
-      ( crab nfv nfrab1 cv wcel wa simprr jca ex rabid 3imtr4g ssrd ) ACBCDGZBC
-      EGZACHBCDIBCEIACJZDKZBLZUAEKZBLZUASKUATKAUCUEAUCLUDBFAUBBMNOBCDPBCEPQR $.
-  $}
-
   $( Intersection with an intersection.  (Contributed by Thierry Arnoux,
      27-Dec-2016.) $)
   inin $p |- ( A i^i ( A i^i B ) ) = ( A i^i B ) $=
@@ -755372,6 +755372,16 @@ that every function in the sequence can have a different (partial)
         XKYJXLYLMXJOXGVDXJOKXGLWBVTWCWEWFWDWGWHYAXSEXREXPWIXREXPWJWKWPXMEXPWLWM
         XIXGBWNGZXQYRXQUHDXEDBEWOWQWRWSXGXDXEWTXAXB $.
     $}
+
+    ${
+      $d S a $.  $d T a $.
+      $( There is a finite number of strictly increasing sequences over finite
+         alphabet.  (Contributed by Ender Ting, 5-Jan-2024.) $)
+      upwrdfi $p |- ( S e. Fin -> { a e. UpWord S | ( # ` a ) = T } e. Fin ) $=
+        ( cfn wcel cv chash cfv wceq cword crab cupword wrdnfi wss upwordisword
+        wtru ad2antrl rabss3d mptru ssfi mpan2 syl ) ADZECFZGHBIZCAJZKZUCEZUECA
+        LZKZUCEZCBAMUHUJUGNZUKULPZUECUIUFUDUIEUDUFEUMUEUDAOQRSUGUJTUAUB $.
+    $}
   $}
 
   $(