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 biimpi 
 |-  ( b e. U -> b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) )
51 50 adantl 
 |-  ( ( ph /\ b e. U ) -> b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) )
52 eliun 
 |-  ( b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) <-> E. w e. Word A b e. ( { w } X. ( 0 ... ( # ` w ) ) ) )
53 51 52 sylib 
 |-  ( ( ph /\ b e. U ) -> E. w e. Word A b e. ( { w } X. ( 0 ... ( # ` w ) ) ) )
54 sneq 
 |-  ( u = w -> { u } = { w } )
55 fveq2 
 |-  ( u = w -> ( # ` u ) = ( # ` w ) )
56 55 oveq2d 
 |-  ( u = w -> ( 0 ... ( # ` u ) ) = ( 0 ... ( # ` w ) ) )
57 54 56 xpeq12d 
 |-  ( u = w -> ( { u } X. ( 0 ... ( # ` u ) ) ) = ( { w } X. ( 0 ... ( # ` w ) ) ) )
58 57 eleq2d 
 |-  ( u = w -> ( b e. ( { u } X. ( 0 ... ( # ` u ) ) ) <-> b e. ( { w } X. ( 0 ... ( # ` w ) ) ) ) )
59 58 cbvrexvw 
 |-  ( E. u e. Word A b e. ( { u } X. ( 0 ... ( # ` u ) ) ) <-> E. w e. Word A b e. ( { w } X. ( 0 ... ( # ` w ) ) ) )
60 53 59 sylibr 
 |-  ( ( ph /\ b e. U ) -> E. u e. Word A b e. ( { u } X. ( 0 ... ( # ` u ) ) ) )
61 48 60 r19.29a 
 |-  ( ( ph /\ b e. U ) -> ( 1st ` b ) e. Word A )
62 pfxcl 
 |-  ( ( 1st ` b ) e. Word A -> ( ( 1st ` b ) prefix ( 2nd ` b ) ) e. Word A )
63 61 62 syl 
 |-  ( ( ph /\ b e. U ) -> ( ( 1st ` b ) prefix ( 2nd ` b ) ) e. Word A )
64 swrdcl 
 |-  ( ( 1st ` b ) e. Word A -> ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) e. Word A )
65 61 64 syl 
 |-  ( ( ph /\ b e. U ) -> ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) e. Word A )
66 63 65 opelxpd 
 |-  ( ( ph /\ b e. U ) -> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. e. ( Word A X. Word A ) )
67 51 adantr 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> b e. U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) )
68 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 ) ) ) ) )
69 67 68 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 ) ) ) ) )
70 opeq1 
 |-  ( u = w -> <. u , n >. = <. w , n >. )
71 70 eqeq2d 
 |-  ( u = w -> ( b = <. u , n >. <-> b = <. w , n >. ) )
72 eleq1w 
 |-  ( u = w -> ( u e. Word A <-> w e. Word A ) )
73 56 eleq2d 
 |-  ( u = w -> ( n e. ( 0 ... ( # ` u ) ) <-> n e. ( 0 ... ( # ` w ) ) ) )
74 72 73 anbi12d 
 |-  ( u = w -> ( ( u e. Word A /\ n e. ( 0 ... ( # ` u ) ) ) <-> ( w e. Word A /\ n e. ( 0 ... ( # ` w ) ) ) ) )
75 71 74 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 ) ) ) ) ) )
76 75 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 ) ) ) ) ) )
77 76 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 ) ) ) ) )
78 69 77 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 ) ) ) ) )
79 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 ) ) )
80 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 ) ) >. ) )
81 79 80 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 ) ) >. ) ) )
82 vex 
 |-  u e. _V
83 vex 
 |-  n e. _V
84 82 83 op1std 
 |-  ( b = <. u , n >. -> ( 1st ` b ) = u )
85 84 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 )
86 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 )
87 85 86 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 )
88 82 83 op2ndd 
 |-  ( b = <. u , n >. -> ( 2nd ` b ) = n )
89 88 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 )
90 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 ) ) )
91 85 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 ) )
92 91 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 ) ) )
93 92 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 ) ) ) )
94 90 93 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 ) ) ) )
95 89 94 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 ) ) ) )
96 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 ) )
97 87 95 96 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 ) )
98 81 97 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 ) ) )
99 79 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 ) ) ) )
100 pfxlen 
 |-  ( ( ( 1st ` b ) e. Word A /\ ( 2nd ` b ) e. ( 0 ... ( # ` ( 1st ` b ) ) ) ) -> ( # ` ( ( 1st ` b ) prefix ( 2nd ` b ) ) ) = ( 2nd ` b ) )
101 87 95 100 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 ) )
102 99 101 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 ) ) )
103 98 102 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 ) ) ) )
104 103 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 ) ) ) )
105 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 ) ) )
106 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 ) ) )
107 105 106 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 ) ) ) )
108 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 )
109 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 )
110 pfxccat1 
 |-  ( ( ( 1st ` a ) e. Word A /\ ( 2nd ` a ) e. Word A ) -> ( ( ( 1st ` a ) ++ ( 2nd ` a ) ) prefix ( # ` ( 1st ` a ) ) ) = ( 1st ` a ) )
111 108 109 110 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 ) )
112 107 111 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 ) ) )
113 105 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 ) ) ) )
114 108 109 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 ) ) ) )
115 113 114 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 ) ) ) )
116 106 115 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 ) ) ) >. )
117 105 116 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 ) ) ) >. ) )
118 swrdccat2 
 |-  ( ( ( 1st ` a ) e. Word A /\ ( 2nd ` a ) e. Word A ) -> ( ( ( 1st ` a ) ++ ( 2nd ` a ) ) substr <. ( # ` ( 1st ` a ) ) , ( ( # ` ( 1st ` a ) ) + ( # ` ( 2nd ` a ) ) ) >. ) = ( 2nd ` a ) )
119 108 109 118 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 ) )
120 117 119 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 ) ) >. ) )
121 112 120 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 ) ) >. ) ) )
122 121 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 ) ) >. ) ) )
123 104 122 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 ) ) ) ) )
124 123 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 ) ) ) ) )
125 124 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 ) ) ) ) ) )
126 125 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 ) ) ) ) ) )
127 126 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 ) ) ) ) ) )
128 127 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 ) ) ) ) )
129 78 128 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 ) ) ) ) )
130 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 ) ) >. ) ) ) )
131 130 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 ) ) >. ) ) ) )
132 snssi 
 |-  ( w e. Word A -> { w } C_ Word A )
133 132 adantl 
 |-  ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ w e. Word A ) -> { w } C_ Word A )
134 fz0ssnn0 
 |-  ( 0 ... ( # ` w ) ) C_ NN0
135 xpss12 
 |-  ( ( { w } C_ Word A /\ ( 0 ... ( # ` w ) ) C_ NN0 ) -> ( { w } X. ( 0 ... ( # ` w ) ) ) C_ ( Word A X. NN0 ) )
136 133 134 135 sylancl 
 |-  ( ( ( ph /\ a e. ( Word A X. Word A ) ) /\ w e. Word A ) -> ( { w } X. ( 0 ... ( # ` w ) ) ) C_ ( Word A X. NN0 ) )
137 136 iunssd 
 |-  ( ( ph /\ a e. ( Word A X. Word A ) ) -> U_ w e. Word A ( { w } X. ( 0 ... ( # ` w ) ) ) C_ ( Word A X. NN0 ) )
138 137 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 ) )
139 138 67 sseldd 
 |-  ( ( ( ph /\ b e. U ) /\ a e. ( Word A X. Word A ) ) -> b e. ( Word A X. NN0 ) )
140 eqop 
 |-  ( b e. ( Word A X. NN0 ) -> ( b = <. ( ( 1st ` a ) ++ ( 2nd ` a ) ) , ( # ` ( 1st ` a ) ) >. <-> ( ( 1st ` b ) = ( ( 1st ` a ) ++ ( 2nd ` a ) ) /\ ( 2nd ` b ) = ( # ` ( 1st ` a ) ) ) ) )
141 139 140 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 ) ) ) ) )
142 129 131 141 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 ) ) >. ) )
143 142 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 ) ) >. ) )
144 143 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 ) ) >. ) )
145 2 41 66 144 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 ) ) >. ) >. ) ) )
146 145 simpld 
 |-  ( ph -> F : ( Word A X. Word A ) -1-1-onto-> U )
147 145 simprd 
 |-  ( ph -> `' F = ( b e. U |-> <. ( ( 1st ` b ) prefix ( 2nd ` b ) ) , ( ( 1st ` b ) substr <. ( 2nd ` b ) , ( # ` ( 1st ` b ) ) >. ) >. ) )
148 147 3 eqtr4di 
 |-  ( ph -> `' F = G )
149 146 148 jca 
 |-  ( ph -> ( F : ( Word A X. Word A ) -1-1-onto-> U /\ `' F = G ) )