Theorem wrd2ind 12375

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

Hypotheses

Ref	Expression
wrd2ind.1	|- ( ( x = (/) /\ w = (/) ) -> ( ph <-> ps ) )
wrd2ind.2	|- ( ( x = y /\ w = u ) -> ( ph <-> ch ) )
wrd2ind.3	|- ( ( x = ( y concat <" z "> ) /\ w = ( u concat <" 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

Ref	Expression
wrd2ind	|- ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> ta )

Distinct variable groups:   x, w, A   y, w, z, B, x   u, s, w, x, y, z, X   Y, s, u, w, x, y, z   ch, w, x   ph, s, u, y, z   ta, x   th, w, x   rh, w

Allowed substitution hints:   ph( x, w)   ps( x, y, z, w, u, s)   ch( y, z, u, s)   th( y, z, u, s)   ta( y, z, w, u, s)   rh( x, y, z, u, s)   A( y, z, u, s)   B( u, s)

Proof of Theorem wrd2ind

Dummy variables n m are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		lencl 12252	. . . . 5 |- ( A e. Word X -> ( # ` A ) e. NN0 )
2		eqeq2 2452	. . . . . . . . 9 |- ( n = 0 -> ( ( # ` x ) = n <-> ( # ` x ) = 0 ) )
3	2	anbi2d 703	. . . . . . . 8 |- ( n = 0 -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) <-> ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = 0 ) ) )
4	3	imbi1d 317	. . . . . . 7 |- ( n = 0 -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = 0 ) -> ph ) ) )
5	4	2ralbidv 2760	. . . . . 6 |- ( 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 ) ) )
6		eqeq2 2452	. . . . . . . . 9 |- ( n = m -> ( ( # ` x ) = n <-> ( # ` x ) = m ) )
7	6	anbi2d 703	. . . . . . . 8 |- ( n = m -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) <-> ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) ) )
8	7	imbi1d 317	. . . . . . 7 |- ( n = m -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) ) )
9	8	2ralbidv 2760	. . . . . 6 |- ( 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 ) ) )
10		eqeq2 2452	. . . . . . . . 9 |- ( n = ( m + 1 ) -> ( ( # ` x ) = n <-> ( # ` x ) = ( m + 1 ) ) )
11	10	anbi2d 703	. . . . . . . 8 |- ( n = ( m + 1 ) -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) <-> ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) )
12	11	imbi1d 317	. . . . . . 7 |- ( n = ( m + 1 ) -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ph ) ) )
13	12	2ralbidv 2760	. . . . . 6 |- ( 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 ) ) )
14		eqeq2 2452	. . . . . . . . 9 |- ( n = ( # ` A ) -> ( ( # ` x ) = n <-> ( # ` x ) = ( # ` A ) ) )
15	14	anbi2d 703	. . . . . . . 8 |- ( n = ( # ` A ) -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) <-> ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) ) )
16	15	imbi1d 317	. . . . . . 7 |- ( n = ( # ` A ) -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = n ) -> ph ) <-> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) ) )
17	16	2ralbidv 2760	. . . . . 6 |- ( 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 ) ) )
18		eqeq1 2449	. . . . . . . . . . . 12 |- ( ( # ` x ) = 0 -> ( ( # ` x ) = ( # ` w ) <-> 0 = ( # ` w ) ) )
19	18	adantl 466	. . . . . . . . . . 11 |- ( ( ( w e. Word Y /\ x e. Word X ) /\ ( # ` x ) = 0 ) -> ( ( # ` x ) = ( # ` w ) <-> 0 = ( # ` w ) ) )
20		eqcom 2445	. . . . . . . . . . . . . . 15 |- ( 0 = ( # ` w ) <-> ( # ` w ) = 0 )
21		hasheq0 12134	. . . . . . . . . . . . . . 15 |- ( w e. Word Y -> ( ( # ` w ) = 0 <-> w = (/) ) )
22	20, 21	syl5bb 257	. . . . . . . . . . . . . 14 |- ( w e. Word Y -> ( 0 = ( # ` w ) <-> w = (/) ) )
23		hasheq0 12134	. . . . . . . . . . . . . . . 16 |- ( x e. Word X -> ( ( # ` x ) = 0 <-> x = (/) ) )
24		wrd2ind.6	. . . . . . . . . . . . . . . . . 18 |- ps
25		wrd2ind.1	. . . . . . . . . . . . . . . . . 18 |- ( ( x = (/) /\ w = (/) ) -> ( ph <-> ps ) )
26	24, 25	mpbiri 233	. . . . . . . . . . . . . . . . 17 |- ( ( x = (/) /\ w = (/) ) -> ph )
27	26	ex 434	. . . . . . . . . . . . . . . 16 |- ( x = (/) -> ( w = (/) -> ph ) )
28	23, 27	syl6bi 228	. . . . . . . . . . . . . . 15 |- ( x e. Word X -> ( ( # ` x ) = 0 -> ( w = (/) -> ph ) ) )
29	28	com13 80	. . . . . . . . . . . . . 14 |- ( w = (/) -> ( ( # ` x ) = 0 -> ( x e. Word X -> ph ) ) )
30	22, 29	syl6bi 228	. . . . . . . . . . . . 13 |- ( w e. Word Y -> ( 0 = ( # ` w ) -> ( ( # ` x ) = 0 -> ( x e. Word X -> ph ) ) ) )
31	30	com24 87	. . . . . . . . . . . 12 |- ( w e. Word Y -> ( x e. Word X -> ( ( # ` x ) = 0 -> ( 0 = ( # ` w ) -> ph ) ) ) )
32	31	imp31 432	. . . . . . . . . . 11 |- ( ( ( w e. Word Y /\ x e. Word X ) /\ ( # ` x ) = 0 ) -> ( 0 = ( # ` w ) -> ph ) )
33	19, 32	sylbid 215	. . . . . . . . . 10 |- ( ( ( w e. Word Y /\ x e. Word X ) /\ ( # ` x ) = 0 ) -> ( ( # ` x ) = ( # ` w ) -> ph ) )
34	33	ex 434	. . . . . . . . 9 |- ( ( w e. Word Y /\ x e. Word X ) -> ( ( # ` x ) = 0 -> ( ( # ` x ) = ( # ` w ) -> ph ) ) )
35	34	com23 78	. . . . . . . 8 |- ( ( w e. Word Y /\ x e. Word X ) -> ( ( # ` x ) = ( # ` w ) -> ( ( # ` x ) = 0 -> ph ) ) )
36	35	impd 431	. . . . . . 7 |- ( ( w e. Word Y /\ x e. Word X ) -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = 0 ) -> ph ) )
37	36	rgen2 2815	. . . . . 6 |- A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = 0 ) -> ph )
38		fveq2 5694	. . . . . . . . . . . . 13 |- ( x = y -> ( # ` x ) = ( # ` y ) )
39		fveq2 5694	. . . . . . . . . . . . 13 |- ( w = u -> ( # ` w ) = ( # ` u ) )
40	38, 39	eqeqan12d 2458	. . . . . . . . . . . 12 |- ( ( x = y /\ w = u ) -> ( ( # ` x ) = ( # ` w ) <-> ( # ` y ) = ( # ` u ) ) )
41	38	eqeq1d 2451	. . . . . . . . . . . . 13 |- ( x = y -> ( ( # ` x ) = m <-> ( # ` y ) = m ) )
42	41	adantr 465	. . . . . . . . . . . 12 |- ( ( x = y /\ w = u ) -> ( ( # ` x ) = m <-> ( # ` y ) = m ) )
43	40, 42	anbi12d 710	. . . . . . . . . . 11 |- ( ( x = y /\ w = u ) -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) <-> ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) ) )
44		wrd2ind.2	. . . . . . . . . . 11 |- ( ( x = y /\ w = u ) -> ( ph <-> ch ) )
45	43, 44	imbi12d 320	. . . . . . . . . 10 |- ( ( x = y /\ w = u ) -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) <-> ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) )
46	45	ancoms 453	. . . . . . . . 9 |- ( ( w = u /\ x = y ) -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) <-> ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) )
47	46	cbvraldva 2956	. . . . . . . 8 |- ( w = u -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = m ) -> ph ) <-> A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) ) )
48	47	cbvralv 2950	. . . . . . 7 |- ( 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 ) )
49		swrdcl 12318	. . . . . . . . . . . . . . . . 17 |- ( w e. Word Y -> ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) e. Word Y )
50	49	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( w e. Word Y /\ x e. Word X ) -> ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) e. Word Y )
51	50	ad2antrl 727	. . . . . . . . . . . . . . 15 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) e. Word Y )
52		wrdf 12243	. . . . . . . . . . . . . . . . . 18 |- ( w e. Word Y -> w : ( 0..^ ( # ` w ) ) --> Y )
53	52	adantr 465	. . . . . . . . . . . . . . . . 17 |- ( ( w e. Word Y /\ x e. Word X ) -> w : ( 0..^ ( # ` w ) ) --> Y )
54	53	ad2antrl 727	. . . . . . . . . . . . . . . 16 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> w : ( 0..^ ( # ` w ) ) --> Y )
55		eqeq1 2449	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( # ` x ) = ( m + 1 ) -> ( ( # ` x ) = ( # ` w ) <-> ( m + 1 ) = ( # ` w ) ) )
56		nn0p1nn 10622	. . . . . . . . . . . . . . . . . . . . . 22 |- ( m e. NN0 -> ( m + 1 ) e. NN )
57		eleq1 2503	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( # ` w ) = ( m + 1 ) -> ( ( # ` w ) e. NN <-> ( m + 1 ) e. NN ) )
58	57	eqcoms 2446	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( m + 1 ) = ( # ` w ) -> ( ( # ` w ) e. NN <-> ( m + 1 ) e. NN ) )
59	56, 58	syl5ibr 221	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( m + 1 ) = ( # ` w ) -> ( m e. NN0 -> ( # ` w ) e. NN ) )
60	55, 59	syl6bi 228	. . . . . . . . . . . . . . . . . . . 20 |- ( ( # ` x ) = ( m + 1 ) -> ( ( # ` x ) = ( # ` w ) -> ( m e. NN0 -> ( # ` w ) e. NN ) ) )
61	60	impcom 430	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ( m e. NN0 -> ( # ` w ) e. NN ) )
62	61	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) -> ( m e. NN0 -> ( # ` w ) e. NN ) )
63	62	impcom 430	. . . . . . . . . . . . . . . . 17 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` w ) e. NN )
64		fzo0end 11622	. . . . . . . . . . . . . . . . 17 |- ( ( # ` w ) e. NN -> ( ( # ` w ) - 1 ) e. ( 0..^ ( # ` w ) ) )
65	63, 64	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` w ) - 1 ) e. ( 0..^ ( # ` w ) ) )
66	54, 65	ffvelrnd 5847	. . . . . . . . . . . . . . 15 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( w ` ( ( # ` w ) - 1 ) ) e. Y )
67	51, 66	jca 532	. . . . . . . . . . . . . 14 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) e. Word Y /\ ( w ` ( ( # ` w ) - 1 ) ) e. Y ) )
68		swrdcl 12318	. . . . . . . . . . . . . . . 16 |- ( x e. Word X -> ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) e. Word X )
69	68	adantl 466	. . . . . . . . . . . . . . 15 |- ( ( w e. Word Y /\ x e. Word X ) -> ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) e. Word X )
70	69	ad2antrl 727	. . . . . . . . . . . . . 14 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) e. Word X )
71		wrdf 12243	. . . . . . . . . . . . . . . . 17 |- ( x e. Word X -> x : ( 0..^ ( # ` x ) ) --> X )
72	71	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( w e. Word Y /\ x e. Word X ) -> x : ( 0..^ ( # ` x ) ) --> X )
73	72	ad2antrl 727	. . . . . . . . . . . . . . 15 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> x : ( 0..^ ( # ` x ) ) --> X )
74		eleq1 2503	. . . . . . . . . . . . . . . . . . 19 |- ( ( # ` x ) = ( m + 1 ) -> ( ( # ` x ) e. NN <-> ( m + 1 ) e. NN ) )
75	56, 74	syl5ibr 221	. . . . . . . . . . . . . . . . . 18 |- ( ( # ` x ) = ( m + 1 ) -> ( m e. NN0 -> ( # ` x ) e. NN ) )
76	75	ad2antll 728	. . . . . . . . . . . . . . . . 17 |- ( ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) -> ( m e. NN0 -> ( # ` x ) e. NN ) )
77	76	impcom 430	. . . . . . . . . . . . . . . 16 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( # ` x ) e. NN )
78		fzo0end 11622	. . . . . . . . . . . . . . . 16 |- ( ( # ` x ) e. NN -> ( ( # ` x ) - 1 ) e. ( 0..^ ( # ` x ) ) )
79	77, 78	syl 16	. . . . . . . . . . . . . . 15 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( # ` x ) - 1 ) e. ( 0..^ ( # ` x ) ) )
80	73, 79	ffvelrnd 5847	. . . . . . . . . . . . . 14 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( x ` ( ( # ` x ) - 1 ) ) e. X )
81	67, 70, 80	jca32 535	. . . . . . . . . . . . 13 |- ( ( m e. NN0 /\ ( ( w e. Word Y /\ x e. Word X ) /\ ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) ) ) -> ( ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) e. Word Y /\ ( w ` ( ( # ` w ) - 1 ) ) e. Y ) /\ ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) e. Word X /\ ( x ` ( ( # ` x ) - 1 ) ) e. X ) ) )
82	81	adantlr 714	. . . . . . . . . . . 12 |- ( ( ( 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 substr <. 0 , ( ( # ` w ) - 1 ) >. ) e. Word Y /\ ( w ` ( ( # ` w ) - 1 ) ) e. Y ) /\ ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) e. Word X /\ ( x ` ( ( # ` x ) - 1 ) ) e. X ) ) )
83		simprl 755	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
84		simplr 754	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
85		simprrl 763	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) )
86	85	oveq1d 6109	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) )
87		simprlr 762	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 )
88		fzossfz 11573	. . . . . . . . . . . . . . . . . 18 |- ( 0..^ ( # ` x ) ) C_ ( 0 ... ( # ` x ) )
89		simprrr 764	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) )
90	56	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 )
91	89, 90	eqeltrd 2517	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 )
92	91, 78	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) )
93	88, 92	sseldi 3357	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) )
94		swrd0len 12321	. . . . . . . . . . . . . . . . 17 |- ( ( x e. Word X /\ ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) ) -> ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( ( # ` x ) - 1 ) )
95	87, 93, 94	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( ( # ` x ) - 1 ) )
96		simprll 761	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 )
97		oveq1 6101	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( # ` w ) = ( # ` x ) -> ( ( # ` w ) - 1 ) = ( ( # ` x ) - 1 ) )
98		oveq2 6102	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( # ` w ) = ( # ` x ) -> ( 0 ... ( # ` w ) ) = ( 0 ... ( # ` x ) ) )
99	97, 98	eleq12d 2511	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( # ` w ) = ( # ` x ) -> ( ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) <-> ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) ) )
100	99	eqcoms 2446	. . . . . . . . . . . . . . . . . . . 20 |- ( ( # ` x ) = ( # ` w ) -> ( ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) <-> ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) ) )
101	100	adantr 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ( ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) <-> ( ( # ` x ) - 1 ) e. ( 0 ... ( # ` x ) ) ) )
102	101	ad2antll 728	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) ) ) )
103	93, 102	mpbird 232	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) )
104		swrd0len 12321	. . . . . . . . . . . . . . . . 17 |- ( ( w e. Word Y /\ ( ( # ` w ) - 1 ) e. ( 0 ... ( # ` w ) ) ) -> ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) = ( ( # ` w ) - 1 ) )
105	96, 103, 104	syl2anc 661	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) = ( ( # ` w ) - 1 ) )
106	86, 95, 105	3eqtr4d 2485	. . . . . . . . . . . . . . 15 |- ( ( ( 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 substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) )
107	89	oveq1d 6109	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 ) )
108		nn0cn 10592	. . . . . . . . . . . . . . . . . 18 |- ( m e. NN0 -> m e. CC )
109	108	ad2antrr 725	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 )
110		ax-1cn 9343	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
111		pncan 9619	. . . . . . . . . . . . . . . . 17 |- ( ( m e. CC /\ 1 e. CC ) -> ( ( m + 1 ) - 1 ) = m )
112	109, 110, 111	sylancl 662	. . . . . . . . . . . . . . . 16 |- ( ( ( 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 )
113	95, 107, 112	3eqtrd 2479	. . . . . . . . . . . . . . 15 |- ( ( ( 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 substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = m )
114	106, 113	jca 532	. . . . . . . . . . . . . 14 |- ( ( ( 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 substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = m ) )
115	69	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) -> ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) e. Word X )
116		fveq2 5694	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( # ` y ) = ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) )
117		fveq2 5694	. . . . . . . . . . . . . . . . . . . . . 22 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( # ` u ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) )
118	116, 117	eqeqan12d 2458	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) )
119	118	expcom 435	. . . . . . . . . . . . . . . . . . . 20 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) ) )
120	119	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) -> ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) ) )
121	120	imp 429	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) )
122	116	eqeq1d 2451	. . . . . . . . . . . . . . . . . . 19 |- ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( ( # ` y ) = m <-> ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = m ) )
123	122	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) -> ( ( # ` y ) = m <-> ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = m ) )
124	121, 123	anbi12d 710	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) -> ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) <-> ( ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = m ) ) )
125		vex 2978	. . . . . . . . . . . . . . . . . . . . 21 |- y e. _V
126		vex 2978	. . . . . . . . . . . . . . . . . . . . 21 |- u e. _V
127	125, 126, 44	sbc2ie 3265	. . . . . . . . . . . . . . . . . . . 20 |- ( [. y / x ]. [. u / w ]. ph <-> ch )
128	127	bicomi 202	. . . . . . . . . . . . . . . . . . 19 |- ( ch <-> [. y / x ]. [. u / w ]. ph )
129	128	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) -> ( ch <-> [. y / x ]. [. u / w ]. ph ) )
130		simpr 461	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) -> y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) )
131	130	sbceq1d 3194	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) -> ( [. y / x ]. [. u / w ]. ph <-> [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. u / w ]. ph ) )
132		dfsbcq 3191	. . . . . . . . . . . . . . . . . . . . 21 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( [. u / w ]. ph <-> [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) )
133	132	sbcbidv 3248	. . . . . . . . . . . . . . . . . . . 20 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. u / w ]. ph <-> [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) )
134	133	adantl 466	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) -> ( [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. u / w ]. ph <-> [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) )
135	134	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) -> ( [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. u / w ]. ph <-> [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) )
136	129, 131, 135	3bitrd 279	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) -> ( ch <-> [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) )
137	124, 136	imbi12d 320	. . . . . . . . . . . . . . . 16 |- ( ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) -> ( ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) <-> ( ( ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = m ) -> [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) ) )
138	115, 137	rspcdv 3079	. . . . . . . . . . . . . . 15 |- ( ( ( w e. Word Y /\ x e. Word X ) /\ u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) -> ( A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) -> ( ( ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = m ) -> [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) ) )
139	50, 138	rspcimdv 3077	. . . . . . . . . . . . . 14 |- ( ( w e. Word Y /\ x e. Word X ) -> ( A. u e. Word Y A. y e. Word X ( ( ( # ` y ) = ( # ` u ) /\ ( # ` y ) = m ) -> ch ) -> ( ( ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = m ) -> [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) ) )
140	83, 84, 114, 139	syl3c 61	. . . . . . . . . . . . 13 |- ( ( ( 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 substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph )
141	140, 106	jca 532	. . . . . . . . . . . 12 |- ( ( ( 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 substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) )
142		dfsbcq 3191	. . . . . . . . . . . . . . . 16 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( [. u / w ]. [. y / x ]. ph <-> [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. [. y / x ]. ph ) )
143		sbccom 3269	. . . . . . . . . . . . . . . 16 |- ( [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. [. y / x ]. ph <-> [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph )
144	142, 143	syl6bb 261	. . . . . . . . . . . . . . 15 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( [. u / w ]. [. y / x ]. ph <-> [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) )
145	117	eqeq2d 2454	. . . . . . . . . . . . . . 15 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( ( # ` y ) = ( # ` u ) <-> ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) )
146	144, 145	anbi12d 710	. . . . . . . . . . . . . 14 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( ( [. u / w ]. [. y / x ]. ph /\ ( # ` y ) = ( # ` u ) ) <-> ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) ) )
147		oveq1 6101	. . . . . . . . . . . . . . 15 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( u concat <" s "> ) = ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" s "> ) )
148	147	sbceq1d 3194	. . . . . . . . . . . . . 14 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( [. ( u concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph <-> [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) )
149	146, 148	imbi12d 320	. . . . . . . . . . . . 13 |- ( u = ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) -> ( ( ( [. u / w ]. [. y / x ]. ph /\ ( # ` y ) = ( # ` u ) ) -> [. ( u concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) <-> ( ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) ) )
150		s1eq 12294	. . . . . . . . . . . . . . . . 17 |- ( s = ( w ` ( ( # ` w ) - 1 ) ) -> <" s "> = <" ( w ` ( ( # ` w ) - 1 ) ) "> )
151	150	oveq2d 6110	. . . . . . . . . . . . . . . 16 |- ( s = ( w ` ( ( # ` w ) - 1 ) ) -> ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" s "> ) = ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) )
152	151	sbceq1d 3194	. . . . . . . . . . . . . . 15 |- ( s = ( w ` ( ( # ` w ) - 1 ) ) -> ( [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph <-> [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) )
153	152	imbi2d 316	. . . . . . . . . . . . . 14 |- ( s = ( w ` ( ( # ` w ) - 1 ) ) -> ( ( ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) <-> ( ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) ) )
154		sbccom 3269	. . . . . . . . . . . . . . . 16 |- ( [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph <-> [. ( y concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph )
155	154	a1i 11	. . . . . . . . . . . . . . 15 |- ( s = ( w ` ( ( # ` w ) - 1 ) ) -> ( [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph <-> [. ( y concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) )
156	155	imbi2d 316	. . . . . . . . . . . . . 14 |- ( s = ( w ` ( ( # ` w ) - 1 ) ) -> ( ( ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) <-> ( ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( y concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) ) )
157	153, 156	bitrd 253	. . . . . . . . . . . . 13 |- ( s = ( w ` ( ( # ` w ) - 1 ) ) -> ( ( ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) <-> ( ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( y concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) ) )
158		dfsbcq 3191	. . . . . . . . . . . . . . 15 |- ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph <-> [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph ) )
159	116	eqeq1d 2451	. . . . . . . . . . . . . . 15 |- ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) <-> ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) )
160	158, 159	anbi12d 710	. . . . . . . . . . . . . 14 |- ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) <-> ( [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) ) )
161		oveq1 6101	. . . . . . . . . . . . . . 15 |- ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( y concat <" z "> ) = ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" z "> ) )
162	161	sbceq1d 3194	. . . . . . . . . . . . . 14 |- ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( [. ( y concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph <-> [. ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) )
163	160, 162	imbi12d 320	. . . . . . . . . . . . 13 |- ( y = ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) -> ( ( ( [. y / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` y ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( y concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) <-> ( ( [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) ) )
164		s1eq 12294	. . . . . . . . . . . . . . . 16 |- ( z = ( x ` ( ( # ` x ) - 1 ) ) -> <" z "> = <" ( x ` ( ( # ` x ) - 1 ) ) "> )
165	164	oveq2d 6110	. . . . . . . . . . . . . . 15 |- ( z = ( x ` ( ( # ` x ) - 1 ) ) -> ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" z "> ) = ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) )
166	165	sbceq1d 3194	. . . . . . . . . . . . . 14 |- ( z = ( x ` ( ( # ` x ) - 1 ) ) -> ( [. ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph <-> [. ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) )
167	166	imbi2d 316	. . . . . . . . . . . . 13 |- ( z = ( x ` ( ( # ` x ) - 1 ) ) -> ( ( ( [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" z "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) <-> ( ( [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) ) )
168		simplr 754	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( y e. Word X /\ z e. X ) )
169		simpll 753	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( u e. Word Y /\ s e. Y ) )
170		simpr 461	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( # ` y ) = ( # ` u ) )
171		wrd2ind.7	. . . . . . . . . . . . . . . . . 18 |- ( ( ( y e. Word X /\ z e. X ) /\ ( u e. Word Y /\ s e. Y ) /\ ( # ` y ) = ( # ` u ) ) -> ( ch -> th ) )
172	168, 169, 170, 171	syl3anc 1218	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( ch -> th ) )
173	44	ancoms 453	. . . . . . . . . . . . . . . . . 18 |- ( ( w = u /\ x = y ) -> ( ph <-> ch ) )
174	126, 125, 173	sbc2ie 3265	. . . . . . . . . . . . . . . . 17 |- ( [. u / w ]. [. y / x ]. ph <-> ch )
175		ovex 6119	. . . . . . . . . . . . . . . . . 18 |- ( u concat <" s "> ) e. _V
176		ovex 6119	. . . . . . . . . . . . . . . . . 18 |- ( y concat <" z "> ) e. _V
177		wrd2ind.3	. . . . . . . . . . . . . . . . . . 19 |- ( ( x = ( y concat <" z "> ) /\ w = ( u concat <" s "> ) ) -> ( ph <-> th ) )
178	177	ancoms 453	. . . . . . . . . . . . . . . . . 18 |- ( ( w = ( u concat <" s "> ) /\ x = ( y concat <" z "> ) ) -> ( ph <-> th ) )
179	175, 176, 178	sbc2ie 3265	. . . . . . . . . . . . . . . . 17 |- ( [. ( u concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph <-> th )
180	172, 174, 179	3imtr4g 270	. . . . . . . . . . . . . . . 16 |- ( ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) /\ ( # ` y ) = ( # ` u ) ) -> ( [. u / w ]. [. y / x ]. ph -> [. ( u concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) )
181	180	ex 434	. . . . . . . . . . . . . . 15 |- ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) -> ( ( # ` y ) = ( # ` u ) -> ( [. u / w ]. [. y / x ]. ph -> [. ( u concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) ) )
182	181	com23 78	. . . . . . . . . . . . . 14 |- ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) -> ( [. u / w ]. [. y / x ]. ph -> ( ( # ` y ) = ( # ` u ) -> [. ( u concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) ) )
183	182	impd 431	. . . . . . . . . . . . 13 |- ( ( ( u e. Word Y /\ s e. Y ) /\ ( y e. Word X /\ z e. X ) ) -> ( ( [. u / w ]. [. y / x ]. ph /\ ( # ` y ) = ( # ` u ) ) -> [. ( u concat <" s "> ) / w ]. [. ( y concat <" z "> ) / x ]. ph ) )
184	149, 157, 163, 167, 183	vtocl4ga 3045	. . . . . . . . . . . 12 |- ( ( ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) e. Word Y /\ ( w ` ( ( # ` w ) - 1 ) ) e. Y ) /\ ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) e. Word X /\ ( x ` ( ( # ` x ) - 1 ) ) e. X ) ) -> ( ( [. ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) / x ]. [. ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) / w ]. ph /\ ( # ` ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) ) = ( # ` ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) ) ) -> [. ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) )
185	82, 141, 184	sylc 60	. . . . . . . . . . 11 |- ( ( ( 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 substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph )
186		eqtr2 2461	. . . . . . . . . . . . . . . 16 |- ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( m + 1 ) ) -> ( # ` w ) = ( m + 1 ) )
187	186	ad2antll 728	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
188	187, 90	eqeltrd 2517	. . . . . . . . . . . . . 14 |- ( ( ( 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 )
189		wrdfin 12251	. . . . . . . . . . . . . . . . 17 |- ( w e. Word Y -> w e. Fin )
190	189	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( w e. Word Y /\ x e. Word X ) -> w e. Fin )
191	190	ad2antrl 727	. . . . . . . . . . . . . . 15 |- ( ( ( 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 )
192		hashnncl 12137	. . . . . . . . . . . . . . 15 |- ( w e. Fin -> ( ( # ` w ) e. NN <-> w =/= (/) ) )
193	191, 192	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( 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 =/= (/) ) )
194	188, 193	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ( 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 =/= (/) )
195		wrdeqcats1 12371	. . . . . . . . . . . . 13 |- ( ( w e. Word Y /\ w =/= (/) ) -> w = ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) )
196	96, 194, 195	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( 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 substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) )
197		wrdfin 12251	. . . . . . . . . . . . . . . . 17 |- ( x e. Word X -> x e. Fin )
198	197	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( w e. Word Y /\ x e. Word X ) -> x e. Fin )
199	198	ad2antrl 727	. . . . . . . . . . . . . . 15 |- ( ( ( 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 )
200		hashnncl 12137	. . . . . . . . . . . . . . 15 |- ( x e. Fin -> ( ( # ` x ) e. NN <-> x =/= (/) ) )
201	199, 200	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( 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 =/= (/) ) )
202	91, 201	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ( 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 =/= (/) )
203		wrdeqcats1 12371	. . . . . . . . . . . . 13 |- ( ( x e. Word X /\ x =/= (/) ) -> x = ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) )
204	87, 202, 203	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( 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 substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) )
205		sbceq1a 3200	. . . . . . . . . . . . 13 |- ( w = ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) -> ( ph <-> [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) )
206		sbceq1a 3200	. . . . . . . . . . . . 13 |- ( x = ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) -> ( [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph <-> [. ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) )
207	205, 206	sylan9bb 699	. . . . . . . . . . . 12 |- ( ( w = ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) /\ x = ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) ) -> ( ph <-> [. ( ( x substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) )
208	196, 204, 207	syl2anc 661	. . . . . . . . . . 11 |- ( ( ( 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 substr <. 0 , ( ( # ` x ) - 1 ) >. ) concat <" ( x ` ( ( # ` x ) - 1 ) ) "> ) / x ]. [. ( ( w substr <. 0 , ( ( # ` w ) - 1 ) >. ) concat <" ( w ` ( ( # ` w ) - 1 ) ) "> ) / w ]. ph ) )
209	185, 208	mpbird 232	. . . . . . . . . 10 |- ( ( ( 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 )
210	209	expr 615	. . . . . . . . 9 |- ( ( ( 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 ) )
211	210	ralrimivva 2811	. . . . . . . 8 |- ( ( 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 ) )
212	211	ex 434	. . . . . . 7 |- ( 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 ) ) )
213	48, 212	syl5bi 217	. . . . . 6 |- ( 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 ) ) )
214	5, 9, 13, 17, 37, 213	nn0ind 10741	. . . . 5 |- ( ( # ` A ) e. NN0 -> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) )
215	1, 214	syl 16	. . . 4 |- ( A e. Word X -> A. w e. Word Y A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) )
216	215	3ad2ant1 1009	. . 3 |- ( ( 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 ) )
217		fveq2 5694	. . . . . . . . 9 |- ( w = B -> ( # ` w ) = ( # ` B ) )
218	217	eqeq2d 2454	. . . . . . . 8 |- ( w = B -> ( ( # ` x ) = ( # ` w ) <-> ( # ` x ) = ( # ` B ) ) )
219	218	anbi1d 704	. . . . . . 7 |- ( w = B -> ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) <-> ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) ) )
220		wrd2ind.5	. . . . . . 7 |- ( w = B -> ( ph <-> rh ) )
221	219, 220	imbi12d 320	. . . . . 6 |- ( w = B -> ( ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) <-> ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) ) )
222	221	ralbidv 2738	. . . . 5 |- ( w = B -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` w ) /\ ( # ` x ) = ( # ` A ) ) -> ph ) <-> A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) ) )
223	222	rspcv 3072	. . . 4 |- ( 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 ) ) )
224	223	3ad2ant2 1010	. . 3 |- ( ( 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 ) ) )
225	216, 224	mpd 15	. 2 |- ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) )
226		eqidd 2444	. 2 |- ( ( A e. Word X /\ B e. Word Y /\ ( # ` A ) = ( # ` B ) ) -> ( # ` A ) = ( # ` A ) )
227		fveq2 5694	. . . . . . . . . . 11 |- ( x = A -> ( # ` x ) = ( # ` A ) )
228	227	eqeq1d 2451	. . . . . . . . . 10 |- ( x = A -> ( ( # ` x ) = ( # ` B ) <-> ( # ` A ) = ( # ` B ) ) )
229	227	eqeq1d 2451	. . . . . . . . . 10 |- ( x = A -> ( ( # ` x ) = ( # ` A ) <-> ( # ` A ) = ( # ` A ) ) )
230	228, 229	anbi12d 710	. . . . . . . . 9 |- ( x = A -> ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) <-> ( ( # ` A ) = ( # ` B ) /\ ( # ` A ) = ( # ` A ) ) ) )
231		wrd2ind.4	. . . . . . . . 9 |- ( x = A -> ( rh <-> ta ) )
232	230, 231	imbi12d 320	. . . . . . . 8 |- ( x = A -> ( ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) <-> ( ( ( # ` A ) = ( # ` B ) /\ ( # ` A ) = ( # ` A ) ) -> ta ) ) )
233	232	rspcv 3072	. . . . . . 7 |- ( A e. Word X -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) -> ( ( ( # ` A ) = ( # ` B ) /\ ( # ` A ) = ( # ` A ) ) -> ta ) ) )
234	233	com23 78	. . . . . 6 |- ( A e. Word X -> ( ( ( # ` A ) = ( # ` B ) /\ ( # ` A ) = ( # ` A ) ) -> ( A. x e. Word X ( ( ( # ` x ) = ( # ` B ) /\ ( # ` x ) = ( # ` A ) ) -> rh ) -> ta ) ) )
235	234	expd 436	. . . . 5 |- ( A e. Word X -> ( ( #