Metamath Proof Explorer

Theorem chnind

Description: Induction over a chain. See nnind for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses chnind.1 
|- ( c = (/) -> ( ps <-> ch ) )
chnind.2 
|- ( c = d -> ( ps <-> th ) )
chnind.3 
|- ( c = ( d ++ <" x "> ) -> ( ps <-> ta ) )
chnind.4 
|- ( c = C -> ( ps <-> et ) )
chnind.6 
|- ( ph -> C e. ( .< Chain A ) )
chnind.7 
|- ( ph -> ch )
chnind.8 
|- ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ th ) -> ta )
Assertion chnind 
|- ( ph -> et )

Proof

Step Hyp Ref Expression
1 chnind.1 
 |-  ( c = (/) -> ( ps <-> ch ) )
2 chnind.2 
 |-  ( c = d -> ( ps <-> th ) )
3 chnind.3 
 |-  ( c = ( d ++ <" x "> ) -> ( ps <-> ta ) )
4 chnind.4 
 |-  ( c = C -> ( ps <-> et ) )
5 chnind.6 
 |-  ( ph -> C e. ( .< Chain A ) )
6 chnind.7 
 |-  ( ph -> ch )
7 chnind.8 
 |-  ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ th ) -> ta )
8 5 chnwrd 
 |-  ( ph -> C e. Word A )
9 id 
 |-  ( ph -> ph )
10 ischn 
 |-  ( C e. ( .< Chain A ) <-> ( C e. Word A /\ A. i e. ( dom C \ { 0 } ) ( C ` ( i - 1 ) ) .< ( C ` i ) ) )
11 5 10 sylib 
 |-  ( ph -> ( C e. Word A /\ A. i e. ( dom C \ { 0 } ) ( C ` ( i - 1 ) ) .< ( C ` i ) ) )
12 11 simprd 
 |-  ( ph -> A. i e. ( dom C \ { 0 } ) ( C ` ( i - 1 ) ) .< ( C ` i ) )
13 dmeq 
 |-  ( c = (/) -> dom c = dom (/) )
14 13 difeq1d 
 |-  ( c = (/) -> ( dom c \ { 0 } ) = ( dom (/) \ { 0 } ) )
15 fveq1 
 |-  ( c = (/) -> ( c ` ( i - 1 ) ) = ( (/) ` ( i - 1 ) ) )
16 fveq1 
 |-  ( c = (/) -> ( c ` i ) = ( (/) ` i ) )
17 15 16 breq12d 
 |-  ( c = (/) -> ( ( c ` ( i - 1 ) ) .< ( c ` i ) <-> ( (/) ` ( i - 1 ) ) .< ( (/) ` i ) ) )
18 14 17 raleqbidv 
 |-  ( c = (/) -> ( A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) <-> A. i e. ( dom (/) \ { 0 } ) ( (/) ` ( i - 1 ) ) .< ( (/) ` i ) ) )
19 18 anbi2d 
 |-  ( c = (/) -> ( ( ph /\ A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) ) <-> ( ph /\ A. i e. ( dom (/) \ { 0 } ) ( (/) ` ( i - 1 ) ) .< ( (/) ` i ) ) ) )
20 19 1 imbi12d 
 |-  ( c = (/) -> ( ( ( ph /\ A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) ) -> ps ) <-> ( ( ph /\ A. i e. ( dom (/) \ { 0 } ) ( (/) ` ( i - 1 ) ) .< ( (/) ` i ) ) -> ch ) ) )
21 dmeq 
 |-  ( c = d -> dom c = dom d )
22 21 difeq1d 
 |-  ( c = d -> ( dom c \ { 0 } ) = ( dom d \ { 0 } ) )
23 fveq1 
 |-  ( c = d -> ( c ` ( i - 1 ) ) = ( d ` ( i - 1 ) ) )
24 fveq1 
 |-  ( c = d -> ( c ` i ) = ( d ` i ) )
25 23 24 breq12d 
 |-  ( c = d -> ( ( c ` ( i - 1 ) ) .< ( c ` i ) <-> ( d ` ( i - 1 ) ) .< ( d ` i ) ) )
26 22 25 raleqbidv 
 |-  ( c = d -> ( A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) <-> A. i e. ( dom d \ { 0 } ) ( d ` ( i - 1 ) ) .< ( d ` i ) ) )
27 26 anbi2d 
 |-  ( c = d -> ( ( ph /\ A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) ) <-> ( ph /\ A. i e. ( dom d \ { 0 } ) ( d ` ( i - 1 ) ) .< ( d ` i ) ) ) )
28 27 2 imbi12d 
 |-  ( c = d -> ( ( ( ph /\ A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) ) -> ps ) <-> ( ( ph /\ A. i e. ( dom d \ { 0 } ) ( d ` ( i - 1 ) ) .< ( d ` i ) ) -> th ) ) )
29 dmeq 
 |-  ( c = ( d ++ <" x "> ) -> dom c = dom ( d ++ <" x "> ) )
30 29 difeq1d 
 |-  ( c = ( d ++ <" x "> ) -> ( dom c \ { 0 } ) = ( dom ( d ++ <" x "> ) \ { 0 } ) )
31 fveq1 
 |-  ( c = ( d ++ <" x "> ) -> ( c ` ( i - 1 ) ) = ( ( d ++ <" x "> ) ` ( i - 1 ) ) )
32 fveq1 
 |-  ( c = ( d ++ <" x "> ) -> ( c ` i ) = ( ( d ++ <" x "> ) ` i ) )
33 31 32 breq12d 
 |-  ( c = ( d ++ <" x "> ) -> ( ( c ` ( i - 1 ) ) .< ( c ` i ) <-> ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) )
34 30 33 raleqbidv 
 |-  ( c = ( d ++ <" x "> ) -> ( A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) <-> A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) )
35 34 anbi2d 
 |-  ( c = ( d ++ <" x "> ) -> ( ( ph /\ A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) ) <-> ( ph /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) ) )
36 35 3 imbi12d 
 |-  ( c = ( d ++ <" x "> ) -> ( ( ( ph /\ A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) ) -> ps ) <-> ( ( ph /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ta ) ) )
37 dmeq 
 |-  ( c = C -> dom c = dom C )
38 37 difeq1d 
 |-  ( c = C -> ( dom c \ { 0 } ) = ( dom C \ { 0 } ) )
39 fveq1 
 |-  ( c = C -> ( c ` ( i - 1 ) ) = ( C ` ( i - 1 ) ) )
40 fveq1 
 |-  ( c = C -> ( c ` i ) = ( C ` i ) )
41 39 40 breq12d 
 |-  ( c = C -> ( ( c ` ( i - 1 ) ) .< ( c ` i ) <-> ( C ` ( i - 1 ) ) .< ( C ` i ) ) )
42 38 41 raleqbidv 
 |-  ( c = C -> ( A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) <-> A. i e. ( dom C \ { 0 } ) ( C ` ( i - 1 ) ) .< ( C ` i ) ) )
43 42 anbi2d 
 |-  ( c = C -> ( ( ph /\ A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) ) <-> ( ph /\ A. i e. ( dom C \ { 0 } ) ( C ` ( i - 1 ) ) .< ( C ` i ) ) ) )
44 43 4 imbi12d 
 |-  ( c = C -> ( ( ( ph /\ A. i e. ( dom c \ { 0 } ) ( c ` ( i - 1 ) ) .< ( c ` i ) ) -> ps ) <-> ( ( ph /\ A. i e. ( dom C \ { 0 } ) ( C ` ( i - 1 ) ) .< ( C ` i ) ) -> et ) ) )
45 6 adantr 
 |-  ( ( ph /\ A. i e. ( dom (/) \ { 0 } ) ( (/) ` ( i - 1 ) ) .< ( (/) ` i ) ) -> ch )
46 simpllr 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> ph )
47 simp-4l 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> d e. Word A )
48 simpll 
 |-  ( ( ( d e. Word A /\ x e. A ) /\ ph ) -> d e. Word A )
49 simplr 
 |-  ( ( ( d e. Word A /\ x e. A ) /\ ph ) -> x e. A )
50 49 s1cld 
 |-  ( ( ( d e. Word A /\ x e. A ) /\ ph ) -> <" x "> e. Word A )
51 48 50 ccatdmss 
 |-  ( ( ( d e. Word A /\ x e. A ) /\ ph ) -> dom d C_ dom ( d ++ <" x "> ) )
52 51 ssdifd 
 |-  ( ( ( d e. Word A /\ x e. A ) /\ ph ) -> ( dom d \ { 0 } ) C_ ( dom ( d ++ <" x "> ) \ { 0 } ) )
53 52 sselda 
 |-  ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) -> j e. ( dom ( d ++ <" x "> ) \ { 0 } ) )
54 fvoveq1 
 |-  ( i = j -> ( ( d ++ <" x "> ) ` ( i - 1 ) ) = ( ( d ++ <" x "> ) ` ( j - 1 ) ) )
55 fveq2 
 |-  ( i = j -> ( ( d ++ <" x "> ) ` i ) = ( ( d ++ <" x "> ) ` j ) )
56 54 55 breq12d 
 |-  ( i = j -> ( ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) <-> ( ( d ++ <" x "> ) ` ( j - 1 ) ) .< ( ( d ++ <" x "> ) ` j ) ) )
57 56 adantl 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ i = j ) -> ( ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) <-> ( ( d ++ <" x "> ) ` ( j - 1 ) ) .< ( ( d ++ <" x "> ) ` j ) ) )
58 53 57 rspcdv 
 |-  ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) -> ( A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) -> ( ( d ++ <" x "> ) ` ( j - 1 ) ) .< ( ( d ++ <" x "> ) ` j ) ) )
59 58 imp 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( ( d ++ <" x "> ) ` ( j - 1 ) ) .< ( ( d ++ <" x "> ) ` j ) )
60 simp-4l 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> d e. Word A )
61 50 ad2antrr 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> <" x "> e. Word A )
62 lencl 
 |-  ( d e. Word A -> ( # ` d ) e. NN0 )
63 60 62 syl 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( # ` d ) e. NN0 )
64 63 nn0zd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( # ` d ) e. ZZ )
65 fzossrbm1 
 |-  ( ( # ` d ) e. ZZ -> ( 0 ..^ ( ( # ` d ) - 1 ) ) C_ ( 0 ..^ ( # ` d ) ) )
66 64 65 syl 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( 0 ..^ ( ( # ` d ) - 1 ) ) C_ ( 0 ..^ ( # ` d ) ) )
67 fzossz 
 |-  ( 0 ..^ ( # ` d ) ) C_ ZZ
68 simplr 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> j e. ( dom d \ { 0 } ) )
69 68 eldifad 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> j e. dom d )
70 eqidd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( # ` d ) = ( # ` d ) )
71 70 60 wrdfd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> d : ( 0 ..^ ( # ` d ) ) --> A )
72 71 fdmd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> dom d = ( 0 ..^ ( # ` d ) ) )
73 69 72 eleqtrd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> j e. ( 0 ..^ ( # ` d ) ) )
74 67 73 sselid 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> j e. ZZ )
75 eldifsni 
 |-  ( j e. ( dom d \ { 0 } ) -> j =/= 0 )
76 68 75 syl 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> j =/= 0 )
77 fzo1fzo0n0 
 |-  ( j e. ( 1 ..^ ( # ` d ) ) <-> ( j e. ( 0 ..^ ( # ` d ) ) /\ j =/= 0 ) )
78 73 76 77 sylanbrc 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> j e. ( 1 ..^ ( # ` d ) ) )
79 elfzom1b 
 |-  ( ( j e. ZZ /\ ( # ` d ) e. ZZ ) -> ( j e. ( 1 ..^ ( # ` d ) ) <-> ( j - 1 ) e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) )
80 79 biimpa 
 |-  ( ( ( j e. ZZ /\ ( # ` d ) e. ZZ ) /\ j e. ( 1 ..^ ( # ` d ) ) ) -> ( j - 1 ) e. ( 0 ..^ ( ( # ` d ) - 1 ) ) )
81 74 64 78 80 syl21anc 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( j - 1 ) e. ( 0 ..^ ( ( # ` d ) - 1 ) ) )
82 66 81 sseldd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( j - 1 ) e. ( 0 ..^ ( # ` d ) ) )
83 ccatval1 
 |-  ( ( d e. Word A /\ <" x "> e. Word A /\ ( j - 1 ) e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ++ <" x "> ) ` ( j - 1 ) ) = ( d ` ( j - 1 ) ) )
84 60 61 82 83 syl3anc 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( ( d ++ <" x "> ) ` ( j - 1 ) ) = ( d ` ( j - 1 ) ) )
85 ccatval1 
 |-  ( ( d e. Word A /\ <" x "> e. Word A /\ j e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ++ <" x "> ) ` j ) = ( d ` j ) )
86 60 61 73 85 syl3anc 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( ( d ++ <" x "> ) ` j ) = ( d ` j ) )
87 59 84 86 3brtr3d 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ j e. ( dom d \ { 0 } ) ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( d ` ( j - 1 ) ) .< ( d ` j ) )
88 87 an32s 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ j e. ( dom d \ { 0 } ) ) -> ( d ` ( j - 1 ) ) .< ( d ` j ) )
89 88 adantllr 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ j e. ( dom d \ { 0 } ) ) -> ( d ` ( j - 1 ) ) .< ( d ` j ) )
90 89 ralrimiva 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> A. j e. ( dom d \ { 0 } ) ( d ` ( j - 1 ) ) .< ( d ` j ) )
91 90 an32s 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> A. j e. ( dom d \ { 0 } ) ( d ` ( j - 1 ) ) .< ( d ` j ) )
92 ischn 
 |-  ( d e. ( .< Chain A ) <-> ( d e. Word A /\ A. j e. ( dom d \ { 0 } ) ( d ` ( j - 1 ) ) .< ( d ` j ) ) )
93 47 91 92 sylanbrc 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> d e. ( .< Chain A ) )
94 46 93 jca 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> ( ph /\ d e. ( .< Chain A ) ) )
95 simp-4r 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> x e. A )
96 lsw 
 |-  ( d e. Word A -> ( lastS ` d ) = ( d ` ( ( # ` d ) - 1 ) ) )
97 96 ad5antr 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( lastS ` d ) = ( d ` ( ( # ` d ) - 1 ) ) )
98 simp-4l 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> d e. Word A )
99 fzonn0p1 
 |-  ( ( # ` d ) e. NN0 -> ( # ` d ) e. ( 0 ..^ ( ( # ` d ) + 1 ) ) )
100 98 62 99 3syl 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> ( # ` d ) e. ( 0 ..^ ( ( # ` d ) + 1 ) ) )
101 ccatws1len 
 |-  ( d e. Word A -> ( # ` ( d ++ <" x "> ) ) = ( ( # ` d ) + 1 ) )
102 101 ad4antr 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> ( # ` ( d ++ <" x "> ) ) = ( ( # ` d ) + 1 ) )
103 102 eqcomd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> ( ( # ` d ) + 1 ) = ( # ` ( d ++ <" x "> ) ) )
104 ccatws1cl 
 |-  ( ( d e. Word A /\ x e. A ) -> ( d ++ <" x "> ) e. Word A )
105 104 ad3antrrr 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> ( d ++ <" x "> ) e. Word A )
106 103 105 wrdfd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> ( d ++ <" x "> ) : ( 0 ..^ ( ( # ` d ) + 1 ) ) --> A )
107 106 fdmd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> dom ( d ++ <" x "> ) = ( 0 ..^ ( ( # ` d ) + 1 ) ) )
108 100 107 eleqtrrd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> ( # ` d ) e. dom ( d ++ <" x "> ) )
109 simplr 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> -. d = (/) )
110 109 neqned 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> d =/= (/) )
111 hasheq0 
 |-  ( d e. Word A -> ( ( # ` d ) = 0 <-> d = (/) ) )
112 111 necon3bid 
 |-  ( d e. Word A -> ( ( # ` d ) =/= 0 <-> d =/= (/) ) )
113 112 biimpar 
 |-  ( ( d e. Word A /\ d =/= (/) ) -> ( # ` d ) =/= 0 )
114 98 110 113 syl2anc 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> ( # ` d ) =/= 0 )
115 108 114 eldifsnd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> ( # ` d ) e. ( dom ( d ++ <" x "> ) \ { 0 } ) )
116 fvoveq1 
 |-  ( i = ( # ` d ) -> ( ( d ++ <" x "> ) ` ( i - 1 ) ) = ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) )
117 fveq2 
 |-  ( i = ( # ` d ) -> ( ( d ++ <" x "> ) ` i ) = ( ( d ++ <" x "> ) ` ( # ` d ) ) )
118 116 117 breq12d 
 |-  ( i = ( # ` d ) -> ( ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) <-> ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) .< ( ( d ++ <" x "> ) ` ( # ` d ) ) ) )
119 118 adantl 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ i = ( # ` d ) ) -> ( ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) <-> ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) .< ( ( d ++ <" x "> ) ` ( # ` d ) ) ) )
120 115 119 rspcdv 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) -> ( A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) -> ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) .< ( ( d ++ <" x "> ) ` ( # ` d ) ) ) )
121 120 imp 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) .< ( ( d ++ <" x "> ) ` ( # ` d ) ) )
122 48 ad3antrrr 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> d e. Word A )
123 50 ad3antrrr 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> <" x "> e. Word A )
124 122 62 syl 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( # ` d ) e. NN0 )
125 114 adantr 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( # ` d ) =/= 0 )
126 elnnne0 
 |-  ( ( # ` d ) e. NN <-> ( ( # ` d ) e. NN0 /\ ( # ` d ) =/= 0 ) )
127 124 125 126 sylanbrc 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( # ` d ) e. NN )
128 fzo0end 
 |-  ( ( # ` d ) e. NN -> ( ( # ` d ) - 1 ) e. ( 0 ..^ ( # ` d ) ) )
129 127 128 syl 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( ( # ` d ) - 1 ) e. ( 0 ..^ ( # ` d ) ) )
130 ccatval1 
 |-  ( ( d e. Word A /\ <" x "> e. Word A /\ ( ( # ` d ) - 1 ) e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) = ( d ` ( ( # ` d ) - 1 ) ) )
131 122 123 129 130 syl3anc 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) = ( d ` ( ( # ` d ) - 1 ) ) )
132 49 ad3antrrr 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> x e. A )
133 eqidd 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( # ` d ) = ( # ` d ) )
134 ccats1val2 
 |-  ( ( d e. Word A /\ x e. A /\ ( # ` d ) = ( # ` d ) ) -> ( ( d ++ <" x "> ) ` ( # ` d ) ) = x )
135 122 132 133 134 syl3anc 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( ( d ++ <" x "> ) ` ( # ` d ) ) = x )
136 121 131 135 3brtr3d 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( d ` ( ( # ` d ) - 1 ) ) .< x )
137 97 136 eqbrtrd 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ -. d = (/) ) /\ th ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( lastS ` d ) .< x )
138 137 an42ds 
 |-  ( ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) /\ -. d = (/) ) -> ( lastS ` d ) .< x )
139 138 ex 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> ( -. d = (/) -> ( lastS ` d ) .< x ) )
140 139 orrd 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> ( d = (/) \/ ( lastS ` d ) .< x ) )
141 simpr 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> th )
142 94 95 140 141 7 syl1111anc 
 |-  ( ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) /\ th ) -> ta )
143 142 ex 
 |-  ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( th -> ta ) )
144 143 expl 
 |-  ( ( d e. Word A /\ x e. A ) -> ( ( ph /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ( th -> ta ) ) )
145 88 ralrimiva 
 |-  ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> A. j e. ( dom d \ { 0 } ) ( d ` ( j - 1 ) ) .< ( d ` j ) )
146 fvoveq1 
 |-  ( i = j -> ( d ` ( i - 1 ) ) = ( d ` ( j - 1 ) ) )
147 fveq2 
 |-  ( i = j -> ( d ` i ) = ( d ` j ) )
148 146 147 breq12d 
 |-  ( i = j -> ( ( d ` ( i - 1 ) ) .< ( d ` i ) <-> ( d ` ( j - 1 ) ) .< ( d ` j ) ) )
149 148 cbvralvw 
 |-  ( A. i e. ( dom d \ { 0 } ) ( d ` ( i - 1 ) ) .< ( d ` i ) <-> A. j e. ( dom d \ { 0 } ) ( d ` ( j - 1 ) ) .< ( d ` j ) )
150 145 149 sylibr 
 |-  ( ( ( ( d e. Word A /\ x e. A ) /\ ph ) /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> A. i e. ( dom d \ { 0 } ) ( d ` ( i - 1 ) ) .< ( d ` i ) )
151 150 expl 
 |-  ( ( d e. Word A /\ x e. A ) -> ( ( ph /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> A. i e. ( dom d \ { 0 } ) ( d ` ( i - 1 ) ) .< ( d ` i ) ) )
152 144 151 a2and 
 |-  ( ( d e. Word A /\ x e. A ) -> ( ( ( ph /\ A. i e. ( dom d \ { 0 } ) ( d ` ( i - 1 ) ) .< ( d ` i ) ) -> th ) -> ( ( ph /\ A. i e. ( dom ( d ++ <" x "> ) \ { 0 } ) ( ( d ++ <" x "> ) ` ( i - 1 ) ) .< ( ( d ++ <" x "> ) ` i ) ) -> ta ) ) )
153 20 28 36 44 45 152 wrdind 
 |-  ( C e. Word A -> ( ( ph /\ A. i e. ( dom C \ { 0 } ) ( C ` ( i - 1 ) ) .< ( C ` i ) ) -> et ) )
154 153 imp 
 |-  ( ( C e. Word A /\ ( ph /\ A. i e. ( dom C \ { 0 } ) ( C ` ( i - 1 ) ) .< ( C ` i ) ) ) -> et )
155 8 9 12 154 syl12anc 
 |-  ( ph -> et )