Metamath Proof Explorer

Theorem gsumwrd2dccatlem

Description: Lemma for gsumwrd2dccat . Expose a bijection F between (ordered) pairs of words and words with a length of a subword. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses gsumwrd2dccatlem.u 
|- U = U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) )
gsumwrd2dccatlem.f 
|- F = ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. )
gsumwrd2dccatlem.g 
|- G = ( b e. U |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. )
gsumwrd2dccatlem.a 
|- ( ph -> A e. V )
Assertion gsumwrd2dccatlem 
|- ( ph -> ( F : ( Word A X. Word A ) -1-1-onto-> U /\ `' F = G ) )

Proof

Step Hyp Ref Expression
1 gsumwrd2dccatlem.u 
 |-  U = U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) )
2 gsumwrd2dccatlem.f 
 |-  F = ( a e. ( Word A X. Word A ) |-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. )
3 gsumwrd2dccatlem.g 
 |-  G = ( b e. U |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. )
4 gsumwrd2dccatlem.a 
 |-  ( ph -> A e. V )
5 sneq 
 |-  ( w = ( ( 1st ` a ) ++ ( 2nd ` a ) ) -> { w } = { ( ( 1st ` a ) ++ ( 2nd ` a ) ) } )
6 fveq2 
 |-  ( w = ( ( 1st ` a ) ++ ( 2nd ` a ) ) -> ( # ` w ) = ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) )
7 6 oveq2d 
 |-  ( w = ( ( 1st ` a ) ++ ( 2nd ` a ) ) -> ( 0 ... ( # ` w ) ) = ( 0 ... ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) ) )
8 5 7 xpeq12d 
 |-  ( w = ( ( 1st ` a ) ++ ( 2nd ` a ) ) -> ( { w } X. ( 0 ... ( # ` w ) ) ) = ( { ( ( 1st ` a ) ++ ( 2nd ` a ) ) } X. ( 0 ... ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) ) ) )
9 8 eleq2d 
 |-  ( w = ( ( 1st ` a ) ++ ( 2nd ` a ) ) -> ( <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. e. ( { w } X. ( 0 ... ( # ` w ) ) ) <-> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. e. ( { ( ( 1st ` a ) ++ ( 2nd ` a ) ) } X. ( 0 ... ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) ) ) ) )
10 xp1st 
 |-  ( a e. ( Word A X. Word A ) -> ( 1st ` a ) e. Word A )
11 10 adantl 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( 1st ` a ) e. Word A )
12 xp2nd 
 |-  ( a e. ( Word A X. Word A ) -> ( 2nd ` a ) e. Word A )
13 12 adantl 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( 2nd ` a ) e. Word A )
14 ccatcl 
 |-  ( ( ( 1st ` a ) e. Word A /\ ( 2nd ` a ) e. Word A ) -> ( ( 1st ` a ) ++ ( 2nd ` a ) ) e. Word A )
15 11 13 14 syl2anc 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( ( 1st ` a ) ++ ( 2nd ` a ) ) e. Word A )
16 ovex 
 |-  ( ( 1st ` a ) ++ ( 2nd ` a ) ) e. _V
17 16 snid 
 |-  ( ( 1st ` a ) ++ ( 2nd ` a ) ) e. { ( ( 1st ` a ) ++ ( 2nd ` a ) ) }
18 17 a1i 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( ( 1st ` a ) ++ ( 2nd ` a ) ) e. { ( ( 1st ` a ) ++ ( 2nd ` a ) ) } )
19 0zd 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> 0 e. ZZ )
20 lencl 
 |-  ( ( ( 1st ` a ) ++ ( 2nd ` a ) ) e. Word A -> ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) e. NN0 )
21 15 20 syl 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) e. NN0 )
22 21 nn0zd 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) e. ZZ )
23 lencl 
 |-  ( ( 1st ` a ) e. Word A -> ( # ` ( 1st ` a ) ) e. NN0 )
24 11 23 syl 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( 1st ` a ) ) e. NN0 )
25 24 nn0zd 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( 1st ` a ) ) e. ZZ )
26 24 nn0ge0d 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> 0 <_ ( # ` ( 1st ` a ) ) )
27 lencl 
 |-  ( ( 2nd ` a ) e. Word A -> ( # ` ( 2nd ` a ) ) e. NN0 )
28 13 27 syl 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( 2nd ` a ) ) e. NN0 )
29 28 nn0ge0d 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> 0 <_ ( # ` ( 2nd ` a ) ) )
30 24 nn0red 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( 1st ` a ) ) e. RR )
31 28 nn0red 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( 2nd ` a ) ) e. RR )
32 30 31 addge01d 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( 0 <_ ( # ` ( 2nd ` a ) ) <-> ( # ` ( 1st ` a ) ) <_ ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) ) )
33 29 32 mpbid 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( 1st ` a ) ) <_ ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) )
34 ccatlen 
 |-  ( ( ( 1st ` a ) e. Word A /\ ( 2nd ` a ) e. Word A ) -> ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) = ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) )
35 11 13 34 syl2anc 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) = ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) )
36 33 35 breqtrrd 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( 1st ` a ) ) <_ ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) )
37 19 22 25 26 36 elfzd 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( # ` ( 1st ` a ) ) e. ( 0 ... ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) ) )
38 18 37 opelxpd 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. e. ( { ( ( 1st ` a ) ++ ( 2nd ` a ) ) } X. ( 0 ... ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) ) ) )
39 9 15 38 rspcedvdw 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> E. w e. Word A <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. e. ( { w } X. ( 0 ... ( # ` w ) ) ) )
40 39 eliund 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) )
41 40 1 eleqtrrdi 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. e. U )
42 simpr 
 |-  ( ( ( ph /\ u e. Word A ) /\ b e. ( { u } X. ( 0 ... ( # ` u ) ) ) ) -> b e. ( { u } X. ( 0 ... ( # ` u ) ) ) )
43 xp1st 
 |-  ( b e. ( { u } X. ( 0 ... ( # ` u ) ) ) -> ( 1st ` b ) e. { u } )
44 elsni 
 |-  ( ( 1st ` b ) e. { u } -> ( 1st ` b ) = u )
45 42 43 44 3syl 
 |-  ( ( ( ph /\ u e. Word A ) /\ b e. ( { u } X. ( 0 ... ( # ` u ) ) ) ) -> ( 1st ` b ) = u )
46 simplr 
 |-  ( ( ( ph /\ u e. Word A ) /\ b e. ( { u } X. ( 0 ... ( # ` u ) ) ) ) -> u e. Word A )
47 45 46 eqeltrd 
 |-  ( ( ( ph /\ u e. Word A ) /\ b e. ( { u } X. ( 0 ... ( # ` u ) ) ) ) -> ( 1st ` b ) e. Word A )
48 47 adantllr 
 |-  ( ( ( ( ph /\ b e. U ) /\ u e. Word A ) /\ b e. ( { u } X. ( 0 ... ( # ` u ) ) ) ) -> ( 1st ` b ) e. Word A )
49 1 eleq2i 
 |-  ( b e. U <-> b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) )
50 49 bilani 
 |-  ( ( ph /\ b e. U ) -> b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) )
51 eliun 
 |-  ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) <-> E. w e. Word A b e. ( { w } X. ( 0 ... ( # ` w ) ) ) )
52 50 51 sylib 
 |-  ( ( ph /\ b e. U ) -> E. w e. Word A b e. ( { w } X. ( 0 ... ( # ` w ) ) ) )
53 sneq 
 |-  ( u = w -> { u } = { w } )
54 fveq2 
 |-  ( u = w -> ( # ` u ) = ( # ` w ) )
55 54 oveq2d 
 |-  ( u = w -> ( 0 ... ( # ` u ) ) = ( 0 ... ( # ` w ) ) )
56 53 55 xpeq12d 
 |-  ( u = w -> ( { u } X. ( 0 ... ( # ` u ) ) ) = ( { w } X. ( 0 ... ( # ` w ) ) ) )
57 56 eleq2d 
 |-  ( u = w -> ( b e. ( { u } X. ( 0 ... ( # ` u ) ) ) <-> b e. ( { w } X. ( 0 ... ( # ` w ) ) ) ) )
58 57 cbvrexvw 
 |-  ( E. u e. Word A b e. ( { u } X. ( 0 ... ( # ` u ) ) ) <-> E. w e. Word A b e. ( { w } X. ( 0 ... ( # ` w ) ) ) )
59 52 58 sylibr 
 |-  ( ( ph /\ b e. U ) -> E. u e. Word A b e. ( { u } X. ( 0 ... ( # ` u ) ) ) )
60 48 59 r19.29a 
 |-  ( ( ph /\ b e. U ) -> ( 1st ` b ) e. Word A )
61 pfxcl 
 |-  ( ( 1st ` b ) e. Word A -> ( ( 1st ` b ) prefix ( 2nd ` b ) ) e. Word A )
62 60 61 syl 
 |-  ( ( ph /\ b e. U ) -> ( ( 1st ` b ) prefix ( 2nd ` b ) ) e. Word A )
63 swrdcl 
 |-  ( ( 1st ` b ) e. Word A -> ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) e. Word A )
64 60 63 syl 
 |-  ( ( ph /\ b e. U ) -> ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) e. Word A )
65 62 64 opelxpd 
 |-  ( ( ph /\ b e. U ) -> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. e. ( Word A X. Word A ) )
66 50 adantr 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) )
67 eliunxp 
 |-  ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) <-> E. w E. n ( b = <. w , n >. /\ ( w e. Word A /\ n e. ( 0 ... ( # ` w ) ) ) ) )
68 66 67 sylib 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> E. w E. n ( b = <. w , n >. /\ ( w e. Word A /\ n e. ( 0 ... ( # ` w ) ) ) ) )
69 opeq1 
 |-  ( u = w -> <. u , n >. = <. w , n >. )
70 69 eqeq2d 
 |-  ( u = w -> ( b = <. u , n >. <-> b = <. w , n >. ) )
71 eleq1w 
 |-  ( u = w -> ( u e. Word A <-> w e. Word A ) )
72 55 eleq2d 
 |-  ( u = w -> ( n e. ( 0 ... ( # ` u ) ) <-> n e. ( 0 ... ( # ` w ) ) ) )
73 71 72 anbi12d 
 |-  ( u = w -> ( ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) <-> ( w e. Word A /\ n e. ( 0 ... ( # ` w ) ) ) ) )
74 70 73 anbi12d 
 |-  ( u = w -> ( ( b = <. u , n >. /\ ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) ) <-> ( b = <. w , n >. /\ ( w e. Word A /\ n e. ( 0 ... ( # ` w ) ) ) ) ) )
75 74 exbidv 
 |-  ( u = w -> ( E. n ( b = <. u , n >. /\ ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) ) <-> E. n ( b = <. w , n >. /\ ( w e. Word A /\ n e. ( 0 ... ( # ` w ) ) ) ) ) )
76 75 cbvexvw 
 |-  ( E. u E. n ( b = <. u , n >. /\ ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) ) <-> E. w E. n ( b = <. w , n >. /\ ( w e. Word A /\ n e. ( 0 ... ( # ` w ) ) ) ) )
77 68 76 sylibr 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> E. u E. n ( b = <. u , n >. /\ ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) ) )
78 simplr 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) )
79 simpr 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) )
80 78 79 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( ( 1st ` a ) ++ ( 2nd ` a ) ) = ( ( ( 1st ` b ) prefix ( 2nd ` b ) ) ++ ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) )
81 vex 
 |-  u e. _V
82 vex 
 |-  n e. _V
83 81 82 op1std 
 |-  ( b = <. u , n >. -> ( 1st ` b ) = u )
84 83 ad5antlr 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( 1st ` b ) = u )
85 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> u e. Word A )
86 84 85 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( 1st ` b ) e. Word A )
87 81 82 op2ndd 
 |-  ( b = <. u , n >. -> ( 2nd ` b ) = n )
88 87 ad5antlr 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( 2nd ` b ) = n )
89 simpllr 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> n e. ( 0 ... ( # ` u ) ) )
90 84 eqcomd 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> u = ( 1st ` b ) )
91 90 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( # ` u ) = ( # ` ( 1st ` b ) ) )
92 91 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( 0 ... ( # ` u ) ) = ( 0 ... ( # ` ( 1st ` b ) ) ) )
93 89 92 eleqtrd 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> n e. ( 0 ... ( # ` ( 1st ` b ) ) ) )
94 88 93 eqeltrd 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( 2nd ` b ) e. ( 0 ... ( # ` ( 1st ` b ) ) ) )
95 pfxcctswrd 
 |-  ( ( ( 1st ` b ) e. Word A /\ ( 2nd ` b ) e. ( 0 ... ( # ` ( 1st ` b ) ) ) ) -> ( ( ( 1st ` b ) prefix ( 2nd ` b ) ) ++ ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) = ( 1st ` b ) )
96 86 94 95 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( ( ( 1st ` b ) prefix ( 2nd ` b ) ) ++ ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) = ( 1st ` b ) )
97 80 96 eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) )
98 78 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( # ` ( 1st ` a ) ) = ( # ` ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) )
99 pfxlen 
 |-  ( ( ( 1st ` b ) e. Word A /\ ( 2nd ` b ) e. ( 0 ... ( # ` ( 1st ` b ) ) ) ) -> ( # ` ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) = ( 2nd ` b ) )
100 86 94 99 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( # ` ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) = ( 2nd ` b ) )
101 98 100 eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( 2nd ` b ) = ( # ` ( 1st ` a ) ) )
102 97 101 jca 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) -> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) )
103 102 anasss 
 |-  ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) ) -> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) )
104 simplr 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) )
105 simpr 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( 2nd ` b ) = ( # ` ( 1st ` a ) ) )
106 104 105 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( ( 1st ` b ) prefix ( 2nd ` b ) ) = ( ( ( 1st ` a ) ++ ( 2nd ` a ) ) prefix ( # ` ( 1st ` a ) ) ) )
107 11 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( 1st ` a ) e. Word A )
108 13 ad5antr 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( 2nd ` a ) e. Word A )
109 pfxccat1 
 |-  ( ( ( 1st ` a ) e. Word A /\ ( 2nd ` a ) e. Word A ) -> ( ( ( 1st ` a ) ++ ( 2nd ` a ) ) prefix ( # ` ( 1st ` a ) ) ) = ( 1st ` a ) )
110 107 108 109 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( ( ( 1st ` a ) ++ ( 2nd ` a ) ) prefix ( # ` ( 1st ` a ) ) ) = ( 1st ` a ) )
111 106 110 eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) )
112 104 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( # ` ( 1st ` b ) ) = ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) )
113 107 108 34 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( # ` ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) = ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) )
114 112 113 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( # ` ( 1st ` b ) ) = ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) )
115 105 114 opeq12d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. = <. ( # ` ( 1st ` a ) ) , ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) >. )
116 104 115 oveq12d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) = ( ( ( 1st ` a ) ++ ( 2nd ` a ) ) substr <. ( # ` ( 1st ` a ) ) , ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) >. ) )
117 swrdccat2 
 |-  ( ( ( 1st ` a ) e. Word A /\ ( 2nd ` a ) e. Word A ) -> ( ( ( 1st ` a ) ++ ( 2nd ` a ) ) substr <. ( # ` ( 1st ` a ) ) , ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) >. ) = ( 2nd ` a ) )
118 107 108 117 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( ( ( 1st ` a ) ++ ( 2nd ` a ) ) substr <. ( # ` ( 1st ` a ) ) , ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) >. ) = ( 2nd ` a ) )
119 116 118 eqtr2d 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) )
120 111 119 jca 
 |-  ( ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) -> ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) )
121 120 anasss 
 |-  ( ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) /\ ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) -> ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) )
122 103 121 impbida 
 |-  ( ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ u e. Word A ) /\ n e. ( 0 ... ( # ` u ) ) ) -> ( ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) )
123 122 anasss 
 |-  ( ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b = <. u , n >. ) /\ ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) ) -> ( ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) )
124 123 expl 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> ( ( b = <. u , n >. /\ ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) ) -> ( ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) ) )
125 124 adantlr 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> ( ( b = <. u , n >. /\ ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) ) -> ( ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) ) )
126 125 exlimdv 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> ( E. n ( b = <. u , n >. /\ ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) ) -> ( ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) ) )
127 126 imp 
 |-  ( ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) /\ E. n ( b = <. u , n >. /\ ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) ) ) -> ( ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) )
128 77 127 exlimddv 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> ( ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) )
129 eqop 
 |-  ( a e. ( Word A X. Word A ) -> ( a = <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. <-> ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) ) )
130 129 adantl 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> ( a = <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. <-> ( ( 1st ` a ) = ( ( 1st ` b ) prefix ( 2nd ` b ) ) /\ ( 2nd ` a ) = ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) ) ) )
131 snssi 
 |-  ( w e. Word A -> { w } C_ Word A )
132 131 adantl 
 |-  ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ w e. Word A ) -> { w } C_ Word A )
133 fz0ssnn0 
 |-  ( 0 ... ( # ` w ) ) C_ NN0
134 xpss12 
 |-  ( ( { w } C_ Word A /\ ( 0 ... ( # ` w ) ) C_ NN0 ) -> ( { w } X. ( 0 ... ( # ` w ) ) ) C_ ( Word A X. NN0 ) )
135 132 133 134 sylancl 
 |-  ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ w e. Word A ) -> ( { w } X. ( 0 ... ( # ` w ) ) ) C_ ( Word A X. NN0 ) )
136 135 iunssd 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) C_ ( Word A X. NN0 ) )
137 136 adantlr 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) C_ ( Word A X. NN0 ) )
138 137 66 sseldd 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> b e. ( Word A X. NN0 ) )
139 eqop 
 |-  ( b e. ( Word A X. NN0 ) -> ( b = <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) )
140 138 139 syl 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> ( b = <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) )
141 128 130 140 3bitr4d 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> ( a = <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. <-> b = <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) )
142 141 an32s 
 |-  ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ b e. U ) -> ( a = <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. <-> b = <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) )
143 142 anasss 
 |-  ( ( ph /\ ( a e. ( Word A X. Word A ) /\ b e. U ) ) -> ( a = <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. <-> b = <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. ) )
144 2 41 65 143 f1ocnv2d 
 |-  ( ph -> ( F : ( Word A X. Word A ) -1-1-onto-> U /\ `' F = ( b e. U |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) ) )
145 144 simpld 
 |-  ( ph -> F : ( Word A X. Word A ) -1-1-onto-> U )
146 144 simprd 
 |-  ( ph -> `' F = ( b e. U |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) )
147 146 3 eqtr4di 
 |-  ( ph -> `' F = G )
148 145 147 jca 
 |-  ( ph -> ( F : ( Word A X. Word A ) -1-1-onto-> U /\ `' F = G ) )