This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wrd2ind

Description: Perform induction over the structure of two words of the same length. (Contributed by AV, 23-Jan-2019) (Proof shortened by AV, 12-Oct-2022)

Ref Expression
Hypotheses wrd2ind.1 
|- ( ( x = (/) /\ w = (/) ) -> ( ph <-> ps ) )
wrd2ind.2 
|- ( ( x = y /\ w = u ) -> ( ph <-> ch ) )
wrd2ind.3 
|- ( ( x = ( y ++ <" z "> ) /\ w = ( u ++ <" s "> ) ) -> ( ph <-> th ) )
wrd2ind.4 
|- ( x = A -> ( rh <-> ta ) )
wrd2ind.5 
|- ( w = B -> ( ph <-> rh ) )
wrd2ind.6 
|- ps
wrd2ind.7 
|- ( ( ( y e. Word X /\ z e. X ) /\ ( u e. Word Y /\ s e. Y ) /\ ( # ` y ) = ( # ` u ) ) -> ( ch -> th ) )
Assertion wrd2ind 
|- ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> ta )

Proof

Step Hyp Ref Expression
1 wrd2ind.1 
 |-  ( ( x = (/) /\ w = (/) ) -> ( ph <-> ps ) )
2 wrd2ind.2 
 |-  ( ( x = y /\ w = u ) -> ( ph <-> ch ) )
3 wrd2ind.3 
 |-  ( ( x = ( y ++ <" z "> ) /\ w = ( u ++ <" s "> ) ) -> ( ph <-> th ) )
4 wrd2ind.4 
 |-  ( x = A -> ( rh <-> ta ) )
5 wrd2ind.5 
 |-  ( w = B -> ( ph <-> rh ) )
6 wrd2ind.6 
 |-  ps
7 wrd2ind.7 
 |-  ( ( ( y e. Word X /\ z e. X ) /\ ( u e. Word Y /\ s e. Y ) /\ ( # ` y ) = ( # ` u ) ) -> ( ch -> th ) )
8 lencl 
 |-  ( A e. Word X -> ( # ` A ) e. NN0 )
9 eqeq2 
 |-  ( n = 0 -> ( ( # ` x ) = n <-> ( # ` x ) = 0 ) )
10 9 anbi2d 
 |-  ( n = 0 -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) <-> ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = 0 ) ) )
11 10 imbi1d 
 |-  ( n = 0 -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = 0 ) -> ph ) ) )
12 11 2ralbidv 
 |-  ( n = 0 -> ( A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = 0 ) -> ph ) ) )
13 eqeq2 
 |-  ( n = m -> ( ( # ` x ) = n <-> ( # ` x ) = m ) )
14 13 anbi2d 
 |-  ( n = m -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) <-> ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) ) )
15 14 imbi1d 
 |-  ( n = m -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) ) )
16 15 2ralbidv 
 |-  ( n = m -> ( A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) ) )
17 eqeq2 
 |-  ( n = ( m + 1 ) -> ( ( # ` x ) = n <-> ( # ` x ) = ( m + 1 ) ) )
18 17 anbi2d 
 |-  ( n = ( m + 1 ) -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) <-> ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) )
19 18 imbi1d 
 |-  ( n = ( m + 1 ) -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ph ) ) )
20 19 2ralbidv 
 |-  ( n = ( m + 1 ) -> ( A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ph ) ) )
21 eqeq2 
 |-  ( n = ( # ` A ) -> ( ( # ` x ) = n <-> ( # ` x ) = ( # ` A ) ) )
22 21 anbi2d 
 |-  ( n = ( # ` A ) -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) <-> ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) ) )
23 22 imbi1d 
 |-  ( n = ( # ` A ) -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) ) )
24 23 2ralbidv 
 |-  ( n = ( # ` A ) -> ( A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) ) )
25 eqeq1 
 |-  ( ( # ` x ) = 0 -> ( ( # ` x ) = ( # ` w ) <-> 0 = ( # ` w ) ) )
26 25 adantl 
 |-  ( ( ( w e. Word Y /\ x e. Word X ) /\ ( # ` x ) = 0 ) -> ( ( # ` x ) = ( # ` w ) <-> 0 = ( # ` w ) ) )
27 eqcom 
 |-  ( 0 = ( # ` w ) <-> ( # ` w ) = 0 )
28 hasheq0 
 |-  ( w e. Word Y -> ( ( # ` w ) = 0 <-> w = (/) ) )
29 27 28 bitrid 
 |-  ( w e. Word Y -> ( 0 = ( # ` w ) <-> w = (/) ) )
30 hasheq0 
 |-  ( x e. Word X -> ( ( # ` x ) = 0 <-> x = (/) ) )
31 6 1 mpbiri 
 |-  ( ( x = (/) /\ w = (/) ) -> ph )
32 31 ex 
 |-  ( x = (/) -> ( w = (/) -> ph ) )
33 30 32 biimtrdi 
 |-  ( x e. Word X -> ( ( # ` x ) = 0 -> ( w = (/) -> ph ) ) )
34 33 com13 
 |-  ( w = (/) -> ( ( # ` x ) = 0 -> ( x e. Word X -> ph ) ) )
35 29 34 biimtrdi 
 |-  ( w e. Word Y -> ( 0 = ( # ` w ) -> ( ( # ` x ) = 0 -> ( x e. Word X -> ph ) ) ) )
36 35 com24 
 |-  ( w e. Word Y -> ( x e. Word X -> ( ( # ` x ) = 0 -> ( 0 = ( # ` w ) -> ph ) ) ) )
37 36 imp31 
 |-  ( ( ( w e. Word Y /\ x e. Word X ) /\ ( # ` x ) = 0 ) -> ( 0 = ( # ` w ) -> ph ) )
38 26 37 sylbid 
 |-  ( ( ( w e. Word Y /\ x e. Word X ) /\ ( # ` x ) = 0 ) -> ( ( # ` x ) = ( # ` w ) -> ph ) )
39 38 ex 
 |-  ( ( w e. Word Y /\ x e. Word X ) -> ( ( # ` x ) = 0 -> ( ( # ` x ) = ( # ` w ) -> ph ) ) )
40 39 impcomd 
 |-  ( ( w e. Word Y /\ x e. Word X ) -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = 0 ) -> ph ) )
41 40 rgen2 
 |-  A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = 0 ) -> ph )
42 fveq2 
 |-  ( x = y -> ( # ` x ) = ( # ` y ) )
43 fveq2 
 |-  ( w = u -> ( # ` w ) = ( # ` u ) )
44 42 43 eqeqan12d 
 |-  ( ( x = y /\ w = u ) -> ( ( # ` x ) = ( # ` w ) <-> ( # ` y ) = ( # ` u ) ) )
45 fveqeq2 
 |-  ( x = y -> ( ( # ` x ) = m <-> ( # ` y ) = m ) )
46 45 adantr 
 |-  ( ( x = y /\ w = u ) -> ( ( # ` x ) = m <-> ( # ` y ) = m ) )
47 44 46 anbi12d 
 |-  ( ( x = y /\ w = u ) -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) <-> ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) ) )
48 47 2 imbi12d 
 |-  ( ( x = y /\ w = u ) -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) <-> ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) )
49 48 ancoms 
 |-  ( ( w = u /\ x = y ) -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) <-> ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) )
50 49 cbvraldva 
 |-  ( w = u -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) <-> A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) )
51 50 cbvralvw 
 |-  ( A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) <-> A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) )
52 pfxcl 
 |-  ( w e. Word Y -> ( w prefix ( ( # ` w ) - 1 ) ) e. Word Y )
53 52 adantr 
 |-  ( ( w e. Word Y /\ x e. Word X ) -> ( w prefix ( ( # ` w ) - 1 ) ) e. Word Y )
54 53 ad2antrl 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( w prefix ( ( # ` w ) - 1 ) ) e. Word Y )
55 simprll 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> w e. Word Y )
56 eqeq1 
 |-  ( ( # ` x ) = ( m + 1 ) -> ( ( # ` x ) = ( # ` w ) <-> ( m + 1 ) = ( # ` w ) ) )
57 nn0p1nn 
 |-  ( m e. NN0 -> ( m + 1 ) e. NN )
58 eleq1 
 |-  ( ( # ` w ) = ( m + 1 ) -> ( ( # ` w ) e. NN <-> ( m + 1 ) e. NN ) )
59 58 eqcoms 
 |-  ( ( m + 1 ) = ( # ` w ) -> ( ( # ` w ) e. NN <-> ( m + 1 ) e. NN ) )
60 57 59 imbitrrid 
 |-  ( ( m + 1 ) = ( # ` w ) -> ( m e. NN0 -> ( # ` w ) e. NN ) )
61 56 60 biimtrdi 
 |-  ( ( # ` x ) = ( m + 1 ) -> ( ( # ` x ) = ( # ` w ) -> ( m e. NN0 -> ( # ` w ) e. NN ) ) )
62 61 impcom 
 |-  ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ( m e. NN0 -> ( # ` w ) e. NN ) )
63 62 adantl 
 |-  ( ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) -> ( m e. NN0 -> ( # ` w ) e. NN ) )
64 63 impcom 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` w ) e. NN )
65 64 nnge1d 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> 1 <_ ( # ` w ) )
66 wrdlenge1n0 
 |-  ( w e. Word Y -> ( w =/= (/) <-> 1 <_ ( # ` w ) ) )
67 55 66 syl 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( w =/= (/) <-> 1 <_ ( # ` w ) ) )
68 65 67 mpbird 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> w =/= (/) )
69 lswcl 
 |-  ( ( w e. Word Y /\ w =/= (/) ) -> ( lastS ` w ) e. Y )
70 55 68 69 syl2anc 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( lastS ` w ) e. Y )
71 54 70 jca 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( w prefix ( ( # ` w ) - 1 ) ) e. Word Y /\ ( lastS ` w ) e. Y ) )
72 pfxcl 
 |-  ( x e. Word X -> ( x prefix ( ( # ` x ) - 1 ) ) e. Word X )
73 72 adantl 
 |-  ( ( w e. Word Y /\ x e. Word X ) -> ( x prefix ( ( # ` x ) - 1 ) ) e. Word X )
74 73 ad2antrl 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( x prefix ( ( # ` x ) - 1 ) ) e. Word X )
75 simprlr 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> x e. Word X )
76 eleq1 
 |-  ( ( # ` x ) = ( m + 1 ) -> ( ( # ` x ) e. NN <-> ( m + 1 ) e. NN ) )
77 57 76 imbitrrid 
 |-  ( ( # ` x ) = ( m + 1 ) -> ( m e. NN0 -> ( # ` x ) e. NN ) )
78 77 ad2antll 
 |-  ( ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) -> ( m e. NN0 -> ( # ` x ) e. NN ) )
79 78 impcom 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` x ) e. NN )
80 79 nnge1d 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> 1 <_ ( # ` x ) )
81 wrdlenge1n0 
 |-  ( x e. Word X -> ( x =/= (/) <-> 1 <_ ( # ` x ) ) )
82 75 81 syl 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( x =/= (/) <-> 1 <_ ( # ` x ) ) )
83 80 82 mpbird 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> x =/= (/) )
84 lswcl 
 |-  ( ( x e. Word X /\ x =/= (/) ) -> ( lastS ` x ) e. X )
85 75 83 84 syl2anc 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( lastS ` x ) e. X )
86 71 74 85 jca32 
 |-  ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( ( w prefix ( ( # ` w ) - 1 ) ) e. Word Y /\ ( lastS ` w ) e. Y ) /\ ( ( x prefix ( ( # ` x ) - 1 ) ) e. Word X /\ ( lastS ` x ) e. X ) ) )
87 86 adantlr 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( ( w prefix ( ( # ` w ) - 1 ) ) e. Word Y /\ ( lastS ` w ) e. Y ) /\ ( ( x prefix ( ( # ` x ) - 1 ) ) e. Word X /\ ( lastS ` x ) e. X ) ) )
88 simprl 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( w e. Word Y /\ x e. Word X ) )
89 simplr 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) )
90 simprrl 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` x ) = ( # ` w ) )
91 90 oveq1d 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` x ) - 1 ) = ( ( # ` w ) - 1 ) )
92 simprlr 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> x e. Word X )
93 fzossfz 
 |-  ( 0 ..^ ( # ` x ) ) C_ ( 0 ... ( # ` x ) )
94 simprrr 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` x ) = ( m + 1 ) )
95 57 ad2antrr 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( m + 1 ) e. NN )
96 94 95 eqeltrd 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` x ) e. NN )
97 fzo0end 
 |-  ( ( # ` x ) e. NN -> ( ( # ` x ) - 1 ) e. ( 0 ..^ ( # ` x ) ) )
98 96 97 syl 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` x ) - 1 ) e. ( 0 ..^ ( # ` x ) ) )
99 93 98 sselid 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) )
100 pfxlen 
 |-  ( ( x e. Word X /\ ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) ) -> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( ( # ` x ) - 1 ) )
101 92 99 100 syl2anc 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( ( # ` x ) - 1 ) )
102 simprll 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> w e. Word Y )
103 oveq1 
 |-  ( ( # ` w ) = ( # ` x ) -> ( ( # ` w ) - 1 ) = ( ( # ` x ) - 1 ) )
104 oveq2 
 |-  ( ( # ` w ) = ( # ` x ) -> ( 0 ... ( # ` w ) ) = ( 0 ... ( # ` x ) ) )
105 103 104 eleq12d 
 |-  ( ( # ` w ) = ( # ` x ) -> ( ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) <-> ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) ) )
106 105 eqcoms 
 |-  ( ( # ` x ) = ( # ` w ) -> ( ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) <-> ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) ) )
107 106 adantr 
 |-  ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ( ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) <-> ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) ) )
108 107 ad2antll 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) <-> ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) ) )
109 99 108 mpbird 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) )
110 pfxlen 
 |-  ( ( w e. Word Y /\ ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) ) -> ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) = ( ( # ` w ) - 1 ) )
111 102 109 110 syl2anc 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) = ( ( # ` w ) - 1 ) )
112 91 101 111 3eqtr4d 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) )
113 94 oveq1d 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` x ) - 1 ) = ( ( m + 1 ) - 1 ) )
114 nn0cn 
 |-  ( m e. NN0 -> m e. CC )
115 114 ad2antrr 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> m e. CC )
116 ax-1cn 
 |-  1 e. CC
117 pncan 
 |-  ( ( m e. CC /\ 1 e. CC ) -> ( ( m + 1 ) - 1 ) = m )
118 115 116 117 sylancl 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( m + 1 ) - 1 ) = m )
119 101 113 118 3eqtrd 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = m )
120 112 119 jca 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = m ) )
121 73 adantr 
 |-  ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) -> ( x prefix ( ( # ` x ) - 1 ) ) e. Word X )
122 fveq2 
 |-  ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( # ` y ) = ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) )
123 fveq2 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( # ` u ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) )
124 122 123 eqeqan12d 
 |-  ( ( y = ( x prefix ( ( # ` x ) - 1 ) ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) )
125 124 expcom 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) ) )
126 125 adantl 
 |-  ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) -> ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) ) )
127 126 imp 
 |-  ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) /\ y = ( x prefix ( ( # ` x ) - 1 ) ) ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) )
128 fveqeq2 
 |-  ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( ( # ` y ) = m <-> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = m ) )
129 128 adantl 
 |-  ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) /\ y = ( x prefix ( ( # ` x ) - 1 ) ) ) -> ( ( # ` y ) = m <-> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = m ) )
130 127 129 anbi12d 
 |-  ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) /\ y = ( x prefix ( ( # ` x ) - 1 ) ) ) -> ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) <-> ( ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = m ) ) )
131 vex 
 |-  y e. _V
132 vex 
 |-  u e. _V
133 131 132 2 sbc2ie 
 |-  ( [. y / x ]. [. u / w ]. ph <-> ch )
134 133 bicomi 
 |-  ( ch <-> [. y / x ]. [. u / w ]. ph )
135 134 a1i 
 |-  ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) /\ y = ( x prefix ( ( # ` x ) - 1 ) ) ) -> ( ch <-> [. y / x ]. [. u / w ]. ph ) )
136 simpr 
 |-  ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) /\ y = ( x prefix ( ( # ` x ) - 1 ) ) ) -> y = ( x prefix ( ( # ` x ) - 1 ) ) )
137 136 sbceq1d 
 |-  ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) /\ y = ( x prefix ( ( # ` x ) - 1 ) ) ) -> ( [. y / x ]. [. u / w ]. ph <-> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. u / w ]. ph ) )
138 dfsbcq 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( [. u / w ]. ph <-> [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) )
139 138 sbcbidv 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. u / w ]. ph <-> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) )
140 139 adantl 
 |-  ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) -> ( [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. u / w ]. ph <-> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) )
141 140 adantr 
 |-  ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) /\ y = ( x prefix ( ( # ` x ) - 1 ) ) ) -> ( [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. u / w ]. ph <-> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) )
142 135 137 141 3bitrd 
 |-  ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) /\ y = ( x prefix ( ( # ` x ) - 1 ) ) ) -> ( ch <-> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) )
143 130 142 imbi12d 
 |-  ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) /\ y = ( x prefix ( ( # ` x ) - 1 ) ) ) -> ( ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) <-> ( ( ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = m ) -> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) ) )
144 121 143 rspcdv 
 |-  ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w prefix ( ( # ` w ) - 1 ) ) ) -> ( A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) -> ( ( ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = m ) -> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) ) )
145 53 144 rspcimdv 
 |-  ( ( w e. Word Y /\ x e. Word X ) -> ( A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) -> ( ( ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = m ) -> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) ) )
146 88 89 120 145 syl3c 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph )
147 146 112 jca 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) )
148 dfsbcq 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( [. u / w ]. [. y / x ]. ph <-> [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. [. y / x ]. ph ) )
149 sbccom 
 |-  ( [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. [. y / x ]. ph <-> [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph )
150 148 149 bitrdi 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( [. u / w ]. [. y / x ]. ph <-> [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) )
151 123 eqeq2d 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) )
152 150 151 anbi12d 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( ( [. u / w ]. [. y / x ]. ph /\ ( # ` y ) = ( # ` u ) ) <-> ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) ) )
153 oveq1 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( u ++ <" s "> ) = ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" s "> ) )
154 153 sbceq1d 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( [. ( u ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph <-> [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) )
155 152 154 imbi12d 
 |-  ( u = ( w prefix ( ( # ` w ) - 1 ) ) -> ( ( ( [. u / w ]. [. y / x ]. ph /\ ( # ` y ) = ( # ` u ) ) -> [. ( u ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) <-> ( ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) ) )
156 s1eq 
 |-  ( s = ( lastS ` w ) -> <" s "> = <" ( lastS ` w ) "> )
157 156 oveq2d 
 |-  ( s = ( lastS ` w ) -> ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" s "> ) = ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) )
158 157 sbceq1d 
 |-  ( s = ( lastS ` w ) -> ( [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph <-> [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) )
159 158 imbi2d 
 |-  ( s = ( lastS ` w ) -> ( ( ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) <-> ( ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) ) )
160 sbccom 
 |-  ( [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph <-> [. ( y ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph )
161 160 a1i 
 |-  ( s = ( lastS ` w ) -> ( [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph <-> [. ( y ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) )
162 161 imbi2d 
 |-  ( s = ( lastS ` w ) -> ( ( ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) <-> ( ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( y ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) ) )
163 159 162 bitrd 
 |-  ( s = ( lastS ` w ) -> ( ( ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) <-> ( ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( y ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) ) )
164 dfsbcq 
 |-  ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph <-> [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph ) )
165 fveqeq2 
 |-  ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) <-> ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) )
166 164 165 anbi12d 
 |-  ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) <-> ( [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) ) )
167 oveq1 
 |-  ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( y ++ <" z "> ) = ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" z "> ) )
168 167 sbceq1d 
 |-  ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( [. ( y ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph <-> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) )
169 166 168 imbi12d 
 |-  ( y = ( x prefix ( ( # ` x ) - 1 ) ) -> ( ( ( [. y / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` y ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( y ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) <-> ( ( [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) ) )
170 s1eq 
 |-  ( z = ( lastS ` x ) -> <" z "> = <" ( lastS ` x ) "> )
171 170 oveq2d 
 |-  ( z = ( lastS ` x ) -> ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" z "> ) = ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) )
172 171 sbceq1d 
 |-  ( z = ( lastS ` x ) -> ( [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph <-> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) )
173 172 imbi2d 
 |-  ( z = ( lastS ` x ) -> ( ( ( [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" z "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) <-> ( ( [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) ) )
174 simplr 
 |-  ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( y e. Word X /\ z e. X ) )
175 simpll 
 |-  ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( u e. Word Y /\ s e. Y ) )
176 simpr 
 |-  ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( # ` y ) = ( # ` u ) )
177 174 175 176 7 syl3anc 
 |-  ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( ch -> th ) )
178 2 ancoms 
 |-  ( ( w = u /\ x = y ) -> ( ph <-> ch ) )
179 132 131 178 sbc2ie 
 |-  ( [. u / w ]. [. y / x ]. ph <-> ch )
180 ovex 
 |-  ( u ++ <" s "> ) e. _V
181 ovex 
 |-  ( y ++ <" z "> ) e. _V
182 3 ancoms 
 |-  ( ( w = ( u ++ <" s "> ) /\ x = ( y ++ <" z "> ) ) -> ( ph <-> th ) )
183 180 181 182 sbc2ie 
 |-  ( [. ( u ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph <-> th )
184 177 179 183 3imtr4g 
 |-  ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( [. u / w ]. [. y / x ]. ph -> [. ( u ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) )
185 184 ex 
 |-  ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) -> ( ( # ` y ) = ( # ` u ) -> ( [. u / w ]. [. y / x ]. ph -> [. ( u ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) ) )
186 185 impcomd 
 |-  ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) -> ( ( [. u / w ]. [. y / x ]. ph /\ ( # ` y ) = ( # ` u ) ) -> [. ( u ++ <" s "> ) / w ]. [. ( y ++ <" z "> ) / x ]. ph ) )
187 155 163 169 173 186 vtocl4ga 
 |-  ( ( ( ( w prefix ( ( # ` w ) - 1 ) ) e. Word Y /\ ( lastS ` w ) e. Y ) /\ ( ( x prefix ( ( # ` x ) - 1 ) ) e. Word X /\ ( lastS ` x ) e. X ) ) -> ( ( [. ( x prefix ( ( # ` x ) - 1 ) ) / x ]. [. ( w prefix ( ( # ` w ) - 1 ) ) / w ]. ph /\ ( # ` ( x prefix ( ( # ` x ) - 1 ) ) ) = ( # ` ( w prefix ( ( # ` w ) - 1 ) ) ) ) -> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) )
188 87 147 187 sylc 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph )
189 eqtr2 
 |-  ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ( # ` w ) = ( m + 1 ) )
190 189 ad2antll 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` w ) = ( m + 1 ) )
191 190 95 eqeltrd 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` w ) e. NN )
192 wrdfin 
 |-  ( w e. Word Y -> w e. Fin )
193 192 adantr 
 |-  ( ( w e. Word Y /\ x e. Word X ) -> w e. Fin )
194 193 ad2antrl 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> w e. Fin )
195 hashnncl 
 |-  ( w e. Fin -> ( ( # ` w ) e. NN <-> w =/= (/) ) )
196 194 195 syl 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` w ) e. NN <-> w =/= (/) ) )
197 191 196 mpbid 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> w =/= (/) )
198 pfxlswccat 
 |-  ( ( w e. Word Y /\ w =/= (/) ) -> ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) = w )
199 198 eqcomd 
 |-  ( ( w e. Word Y /\ w =/= (/) ) -> w = ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) )
200 102 197 199 syl2anc 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> w = ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) )
201 wrdfin 
 |-  ( x e. Word X -> x e. Fin )
202 201 adantl 
 |-  ( ( w e. Word Y /\ x e. Word X ) -> x e. Fin )
203 202 ad2antrl 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> x e. Fin )
204 hashnncl 
 |-  ( x e. Fin -> ( ( # ` x ) e. NN <-> x =/= (/) ) )
205 203 204 syl 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` x ) e. NN <-> x =/= (/) ) )
206 96 205 mpbid 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> x =/= (/) )
207 pfxlswccat 
 |-  ( ( x e. Word X /\ x =/= (/) ) -> ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) = x )
208 207 eqcomd 
 |-  ( ( x e. Word X /\ x =/= (/) ) -> x = ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) )
209 92 206 208 syl2anc 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> x = ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) )
210 sbceq1a 
 |-  ( w = ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) -> ( ph <-> [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) )
211 sbceq1a 
 |-  ( x = ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) -> ( [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph <-> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) )
212 210 211 sylan9bb 
 |-  ( ( w = ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) /\ x = ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) ) -> ( ph <-> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) )
213 200 209 212 syl2anc 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ph <-> [. ( ( x prefix ( ( # ` x ) - 1 ) ) ++ <" ( lastS ` x ) "> ) / x ]. [. ( ( w prefix ( ( # ` w ) - 1 ) ) ++ <" ( lastS ` w ) "> ) / w ]. ph ) )
214 188 213 mpbird 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ph )
215 214 expr 
 |-  ( ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) /\ ( w e. Word Y /\ x e. Word X ) ) -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ph ) )
216 215 ralrimivva 
 |-  ( ( m e. NN0 /\ A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) -> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ph ) )
217 216 ex 
 |-  ( m e. NN0 -> ( A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) -> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ph ) ) )
218 51 217 biimtrid 
 |-  ( m e. NN0 -> ( A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) -> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ph ) ) )
219 12 16 20 24 41 218 nn0ind 
 |-  ( ( # ` A ) e. NN0 -> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) )
220 8 219 syl 
 |-  ( A e. Word X -> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) )
221 220 3ad2ant1 
 |-  ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) )
222 fveq2 
 |-  ( w = B -> ( # ` w ) = ( # ` B ) )
223 222 eqeq2d 
 |-  ( w = B -> ( ( # ` x ) = ( # ` w ) <-> ( # ` x ) = ( # ` B ) ) )
224 223 anbi1d 
 |-  ( w = B -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) <-> ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) ) )
225 224 5 imbi12d 
 |-  ( w = B -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) <-> ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) ) )
226 225 ralbidv 
 |-  ( w = B -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) <-> A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) ) )
227 226 rspcv 
 |-  ( B e. Word Y -> ( A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) -> A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) ) )
228 227 3ad2ant2 
 |-  ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> ( A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) -> A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) ) )
229 221 228 mpd 
 |-  ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) )
230 eqidd 
 |-  ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> ( # ` A ) = ( # ` A ) )
231 fveqeq2 
 |-  ( x = A -> ( ( # ` x ) = ( # ` B ) <-> ( # ` A ) = ( # ` B ) ) )
232 fveqeq2 
 |-  ( x = A -> ( ( # ` x ) = ( # ` A ) <-> ( # ` A ) = ( # ` A ) ) )
233 231 232 anbi12d 
 |-  ( x = A -> ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) <-> ( ( # ` A ) = ( # ` B ) /\ ( # ` A ) = ( # ` A ) ) ) )
234 233 4 imbi12d 
 |-  ( x = A -> ( ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) <-> ( ( ( # ` A ) = ( # ` B ) /\ ( # ` A ) = ( # ` A ) ) -> ta ) ) )
235 234 rspcv 
 |-  ( A e. Word X -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) -> ( ( ( # ` A ) = ( # ` B ) /\ ( # ` A ) = ( # ` A ) ) -> ta ) ) )
236 235 com23 
 |-  ( A e. Word X -> ( ( ( # ` A ) = ( # ` B ) /\ ( # ` A ) = ( # ` A ) ) -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) -> ta ) ) )
237 236 expd 
 |-  ( A e. Word X -> ( ( # ` A ) = ( # ` B ) -> ( ( # ` A ) = ( # ` A ) -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) -> ta ) ) ) )
238 237 com34 
 |-  ( A e. Word X -> ( ( # ` A ) = ( # ` B ) -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) -> ( ( # ` A ) = ( # ` A ) -> ta ) ) ) )
239 238 imp 
 |-  ( ( A e. Word X /\ ( # ` A ) = ( # ` B ) ) -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) -> ( ( # ` A ) = ( # ` A ) -> ta ) ) )
240 239 3adant2 
 |-  ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) -> ( ( # ` A ) = ( # ` A ) -> ta ) ) )
241 229 230 240 mp2d 
 |-  ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> ta )