Metamath Proof Explorer

Theorem chnub

Description: In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025)

Ref Expression
Hypotheses chnub.1 
|- ( ph -> .< Po A )
chnub.2 
|- ( ph -> C e. ( .< Chain A ) )
chnub.3 
|- ( ph -> I e. ( 0 ..^ ( ( # ` C ) - 1 ) ) )
Assertion chnub 
|- ( ph -> ( C ` I ) .< ( lastS ` C ) )

Proof

Step Hyp Ref Expression
1 chnub.1 
 |-  ( ph -> .< Po A )
2 chnub.2 
 |-  ( ph -> C e. ( .< Chain A ) )
3 chnub.3 
 |-  ( ph -> I e. ( 0 ..^ ( ( # ` C ) - 1 ) ) )
4 fveq2 
 |-  ( i = I -> ( C ` i ) = ( C ` I ) )
5 4 breq1d 
 |-  ( i = I -> ( ( C ` i ) .< ( lastS ` C ) <-> ( C ` I ) .< ( lastS ` C ) ) )
6 fveq2 
 |-  ( c = (/) -> ( # ` c ) = ( # ` (/) ) )
7 6 oveq1d 
 |-  ( c = (/) -> ( ( # ` c ) - 1 ) = ( ( # ` (/) ) - 1 ) )
8 7 oveq2d 
 |-  ( c = (/) -> ( 0 ..^ ( ( # ` c ) - 1 ) ) = ( 0 ..^ ( ( # ` (/) ) - 1 ) ) )
9 fveq1 
 |-  ( c = (/) -> ( c ` i ) = ( (/) ` i ) )
10 fveq2 
 |-  ( c = (/) -> ( lastS ` c ) = ( lastS ` (/) ) )
11 9 10 breq12d 
 |-  ( c = (/) -> ( ( c ` i ) .< ( lastS ` c ) <-> ( (/) ` i ) .< ( lastS ` (/) ) ) )
12 8 11 raleqbidv 
 |-  ( c = (/) -> ( A. i e. ( 0 ..^ ( ( # ` c ) - 1 ) ) ( c ` i ) .< ( lastS ` c ) <-> A. i e. ( 0 ..^ ( ( # ` (/) ) - 1 ) ) ( (/) ` i ) .< ( lastS ` (/) ) ) )
13 fveq2 
 |-  ( c = d -> ( # ` c ) = ( # ` d ) )
14 13 oveq1d 
 |-  ( c = d -> ( ( # ` c ) - 1 ) = ( ( # ` d ) - 1 ) )
15 14 oveq2d 
 |-  ( c = d -> ( 0 ..^ ( ( # ` c ) - 1 ) ) = ( 0 ..^ ( ( # ` d ) - 1 ) ) )
16 fveq1 
 |-  ( c = d -> ( c ` i ) = ( d ` i ) )
17 fveq2 
 |-  ( c = d -> ( lastS ` c ) = ( lastS ` d ) )
18 16 17 breq12d 
 |-  ( c = d -> ( ( c ` i ) .< ( lastS ` c ) <-> ( d ` i ) .< ( lastS ` d ) ) )
19 15 18 raleqbidv 
 |-  ( c = d -> ( A. i e. ( 0 ..^ ( ( # ` c ) - 1 ) ) ( c ` i ) .< ( lastS ` c ) <-> A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) )
20 fveq2 
 |-  ( i = j -> ( c ` i ) = ( c ` j ) )
21 20 breq1d 
 |-  ( i = j -> ( ( c ` i ) .< ( lastS ` c ) <-> ( c ` j ) .< ( lastS ` c ) ) )
22 21 cbvralvw 
 |-  ( A. i e. ( 0 ..^ ( ( # ` c ) - 1 ) ) ( c ` i ) .< ( lastS ` c ) <-> A. j e. ( 0 ..^ ( ( # ` c ) - 1 ) ) ( c ` j ) .< ( lastS ` c ) )
23 fveq2 
 |-  ( c = ( d ++ <" x "> ) -> ( # ` c ) = ( # ` ( d ++ <" x "> ) ) )
24 23 oveq1d 
 |-  ( c = ( d ++ <" x "> ) -> ( ( # ` c ) - 1 ) = ( ( # ` ( d ++ <" x "> ) ) - 1 ) )
25 24 oveq2d 
 |-  ( c = ( d ++ <" x "> ) -> ( 0 ..^ ( ( # ` c ) - 1 ) ) = ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) )
26 fveq1 
 |-  ( c = ( d ++ <" x "> ) -> ( c ` j ) = ( ( d ++ <" x "> ) ` j ) )
27 fveq2 
 |-  ( c = ( d ++ <" x "> ) -> ( lastS ` c ) = ( lastS ` ( d ++ <" x "> ) ) )
28 26 27 breq12d 
 |-  ( c = ( d ++ <" x "> ) -> ( ( c ` j ) .< ( lastS ` c ) <-> ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) ) )
29 25 28 raleqbidv 
 |-  ( c = ( d ++ <" x "> ) -> ( A. j e. ( 0 ..^ ( ( # ` c ) - 1 ) ) ( c ` j ) .< ( lastS ` c ) <-> A. j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) ) )
30 22 29 bitrid 
 |-  ( c = ( d ++ <" x "> ) -> ( A. i e. ( 0 ..^ ( ( # ` c ) - 1 ) ) ( c ` i ) .< ( lastS ` c ) <-> A. j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) ) )
31 fveq2 
 |-  ( c = C -> ( # ` c ) = ( # ` C ) )
32 31 oveq1d 
 |-  ( c = C -> ( ( # ` c ) - 1 ) = ( ( # ` C ) - 1 ) )
33 32 oveq2d 
 |-  ( c = C -> ( 0 ..^ ( ( # ` c ) - 1 ) ) = ( 0 ..^ ( ( # ` C ) - 1 ) ) )
34 fveq1 
 |-  ( c = C -> ( c ` i ) = ( C ` i ) )
35 fveq2 
 |-  ( c = C -> ( lastS ` c ) = ( lastS ` C ) )
36 34 35 breq12d 
 |-  ( c = C -> ( ( c ` i ) .< ( lastS ` c ) <-> ( C ` i ) .< ( lastS ` C ) ) )
37 33 36 raleqbidv 
 |-  ( c = C -> ( A. i e. ( 0 ..^ ( ( # ` c ) - 1 ) ) ( c ` i ) .< ( lastS ` c ) <-> A. i e. ( 0 ..^ ( ( # ` C ) - 1 ) ) ( C ` i ) .< ( lastS ` C ) ) )
38 ral0 
 |-  A. i e. (/) ( (/) ` i ) .< ( lastS ` (/) )
39 hash0 
 |-  ( # ` (/) ) = 0
40 39 oveq1i 
 |-  ( ( # ` (/) ) - 1 ) = ( 0 - 1 )
41 df-neg 
 |-  -u 1 = ( 0 - 1 )
42 neg1rr 
 |-  -u 1 e. RR
43 0re 
 |-  0 e. RR
44 neg1lt0 
 |-  -u 1 < 0
45 42 43 44 ltleii 
 |-  -u 1 <_ 0
46 41 45 eqbrtrri 
 |-  ( 0 - 1 ) <_ 0
47 40 46 eqbrtri 
 |-  ( ( # ` (/) ) - 1 ) <_ 0
48 0z 
 |-  0 e. ZZ
49 39 48 eqeltri 
 |-  ( # ` (/) ) e. ZZ
50 1z 
 |-  1 e. ZZ
51 zsubcl 
 |-  ( ( ( # ` (/) ) e. ZZ /\ 1 e. ZZ ) -> ( ( # ` (/) ) - 1 ) e. ZZ )
52 49 50 51 mp2an 
 |-  ( ( # ` (/) ) - 1 ) e. ZZ
53 fzon 
 |-  ( ( 0 e. ZZ /\ ( ( # ` (/) ) - 1 ) e. ZZ ) -> ( ( ( # ` (/) ) - 1 ) <_ 0 <-> ( 0 ..^ ( ( # ` (/) ) - 1 ) ) = (/) ) )
54 48 52 53 mp2an 
 |-  ( ( ( # ` (/) ) - 1 ) <_ 0 <-> ( 0 ..^ ( ( # ` (/) ) - 1 ) ) = (/) )
55 47 54 mpbi 
 |-  ( 0 ..^ ( ( # ` (/) ) - 1 ) ) = (/)
56 55 raleqi 
 |-  ( A. i e. ( 0 ..^ ( ( # ` (/) ) - 1 ) ) ( (/) ` i ) .< ( lastS ` (/) ) <-> A. i e. (/) ( (/) ` i ) .< ( lastS ` (/) ) )
57 38 56 mpbir 
 |-  A. i e. ( 0 ..^ ( ( # ` (/) ) - 1 ) ) ( (/) ` i ) .< ( lastS ` (/) )
58 57 a1i 
 |-  ( ph -> A. i e. ( 0 ..^ ( ( # ` (/) ) - 1 ) ) ( (/) ` i ) .< ( lastS ` (/) ) )
59 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> d e. ( .< Chain A ) )
60 59 chnwrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> d e. Word A )
61 ccatws1len 
 |-  ( d e. Word A -> ( # ` ( d ++ <" x "> ) ) = ( ( # ` d ) + 1 ) )
62 60 61 syl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( # ` ( d ++ <" x "> ) ) = ( ( # ` d ) + 1 ) )
63 simpr 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> d = (/) )
64 63 fveq2d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( # ` d ) = ( # ` (/) ) )
65 64 39 eqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( # ` d ) = 0 )
66 65 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( ( # ` d ) + 1 ) = ( 0 + 1 ) )
67 0p1e1 
 |-  ( 0 + 1 ) = 1
68 67 a1i 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( 0 + 1 ) = 1 )
69 62 66 68 3eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( # ` ( d ++ <" x "> ) ) = 1 )
70 69 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( ( # ` ( d ++ <" x "> ) ) - 1 ) = ( 1 - 1 ) )
71 1m1e0 
 |-  ( 1 - 1 ) = 0
72 70 71 eqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( ( # ` ( d ++ <" x "> ) ) - 1 ) = 0 )
73 72 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) = ( 0 ..^ 0 ) )
74 fzo0 
 |-  ( 0 ..^ 0 ) = (/)
75 73 74 eqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) = (/) )
76 simplr 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) )
77 76 ne0d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) =/= (/) )
78 75 77 pm2.21ddne 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d = (/) ) -> ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) )
79 1 ad7antr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> .< Po A )
80 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> d e. ( .< Chain A ) )
81 80 chnwrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> d e. Word A )
82 81 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> d e. Word A )
83 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> x e. A )
84 83 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> x e. A )
85 ccatws1cl 
 |-  ( ( d e. Word A /\ x e. A ) -> ( d ++ <" x "> ) e. Word A )
86 82 84 85 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( d ++ <" x "> ) e. Word A )
87 lencl 
 |-  ( d e. Word A -> ( # ` d ) e. NN0 )
88 81 87 syl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( # ` d ) e. NN0 )
89 88 nn0zd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( # ` d ) e. ZZ )
90 1zzd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> 1 e. ZZ )
91 89 90 zsubcld 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` d ) - 1 ) e. ZZ )
92 89 peano2zd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` d ) + 1 ) e. ZZ )
93 91 zred 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` d ) - 1 ) e. RR )
94 92 zred 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` d ) + 1 ) e. RR )
95 simpr 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> d =/= (/) )
96 hasheq0 
 |-  ( d e. Word A -> ( ( # ` d ) = 0 <-> d = (/) ) )
97 96 necon3bid 
 |-  ( d e. Word A -> ( ( # ` d ) =/= 0 <-> d =/= (/) ) )
98 97 biimpar 
 |-  ( ( d e. Word A /\ d =/= (/) ) -> ( # ` d ) =/= 0 )
99 81 95 98 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( # ` d ) =/= 0 )
100 elnnne0 
 |-  ( ( # ` d ) e. NN <-> ( ( # ` d ) e. NN0 /\ ( # ` d ) =/= 0 ) )
101 88 99 100 sylanbrc 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( # ` d ) e. NN )
102 101 nnred 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( # ` d ) e. RR )
103 102 ltm1d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` d ) - 1 ) < ( # ` d ) )
104 102 ltp1d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( # ` d ) < ( ( # ` d ) + 1 ) )
105 93 102 94 103 104 lttrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` d ) - 1 ) < ( ( # ` d ) + 1 ) )
106 93 94 105 ltled 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` d ) - 1 ) <_ ( ( # ` d ) + 1 ) )
107 eluz2 
 |-  ( ( ( # ` d ) + 1 ) e. ( ZZ>= ` ( ( # ` d ) - 1 ) ) <-> ( ( ( # ` d ) - 1 ) e. ZZ /\ ( ( # ` d ) + 1 ) e. ZZ /\ ( ( # ` d ) - 1 ) <_ ( ( # ` d ) + 1 ) ) )
108 91 92 106 107 syl3anbrc 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` d ) + 1 ) e. ( ZZ>= ` ( ( # ` d ) - 1 ) ) )
109 fzoss2 
 |-  ( ( ( # ` d ) + 1 ) e. ( ZZ>= ` ( ( # ` d ) - 1 ) ) -> ( 0 ..^ ( ( # ` d ) - 1 ) ) C_ ( 0 ..^ ( ( # ` d ) + 1 ) ) )
110 108 109 syl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( 0 ..^ ( ( # ` d ) - 1 ) ) C_ ( 0 ..^ ( ( # ` d ) + 1 ) ) )
111 110 sselda 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> j e. ( 0 ..^ ( ( # ` d ) + 1 ) ) )
112 82 61 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( # ` ( d ++ <" x "> ) ) = ( ( # ` d ) + 1 ) )
113 112 oveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) = ( 0 ..^ ( ( # ` d ) + 1 ) ) )
114 111 113 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) )
115 wrdsymbcl 
 |-  ( ( ( d ++ <" x "> ) e. Word A /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) -> ( ( d ++ <" x "> ) ` j ) e. A )
116 86 114 115 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( ( d ++ <" x "> ) ` j ) e. A )
117 simplr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> d =/= (/) )
118 lswcl 
 |-  ( ( d e. Word A /\ d =/= (/) ) -> ( lastS ` d ) e. A )
119 82 117 118 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( lastS ` d ) e. A )
120 lswccats1 
 |-  ( ( d e. Word A /\ x e. A ) -> ( lastS ` ( d ++ <" x "> ) ) = x )
121 81 83 120 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( lastS ` ( d ++ <" x "> ) ) = x )
122 121 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( lastS ` ( d ++ <" x "> ) ) = x )
123 122 84 eqeltrd 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( lastS ` ( d ++ <" x "> ) ) e. A )
124 116 119 123 3jca 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( ( ( d ++ <" x "> ) ` j ) e. A /\ ( lastS ` d ) e. A /\ ( lastS ` ( d ++ <" x "> ) ) e. A ) )
125 simplr 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) )
126 61 oveq1d 
 |-  ( d e. Word A -> ( ( # ` ( d ++ <" x "> ) ) - 1 ) = ( ( ( # ` d ) + 1 ) - 1 ) )
127 81 126 syl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` ( d ++ <" x "> ) ) - 1 ) = ( ( ( # ` d ) + 1 ) - 1 ) )
128 101 nncnd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( # ` d ) e. CC )
129 1cnd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> 1 e. CC )
130 128 129 pncand 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( ( # ` d ) + 1 ) - 1 ) = ( # ` d ) )
131 127 130 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( # ` ( d ++ <" x "> ) ) - 1 ) = ( # ` d ) )
132 131 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) = ( 0 ..^ ( # ` d ) ) )
133 125 132 eleqtrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> j e. ( 0 ..^ ( # ` d ) ) )
134 133 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> j e. ( 0 ..^ ( # ` d ) ) )
135 ccats1val1 
 |-  ( ( d e. Word A /\ j e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ++ <" x "> ) ` j ) = ( d ` j ) )
136 82 134 135 syl2anc 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( ( d ++ <" x "> ) ` j ) = ( d ` j ) )
137 fveq2 
 |-  ( i = j -> ( d ` i ) = ( d ` j ) )
138 137 breq1d 
 |-  ( i = j -> ( ( d ` i ) .< ( lastS ` d ) <-> ( d ` j ) .< ( lastS ` d ) ) )
139 simp-4r 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) )
140 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) )
141 138 139 140 rspcdva 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( d ` j ) .< ( lastS ` d ) )
142 136 141 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( ( d ++ <" x "> ) ` j ) .< ( lastS ` d ) )
143 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( d = (/) \/ ( lastS ` d ) .< x ) )
144 95 neneqd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> -. d = (/) )
145 143 144 orcnd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( lastS ` d ) .< x )
146 145 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( lastS ` d ) .< x )
147 146 122 breqtrrd 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( lastS ` d ) .< ( lastS ` ( d ++ <" x "> ) ) )
148 potr 
 |-  ( ( .< Po A /\ ( ( ( d ++ <" x "> ) ` j ) e. A /\ ( lastS ` d ) e. A /\ ( lastS ` ( d ++ <" x "> ) ) e. A ) ) -> ( ( ( ( d ++ <" x "> ) ` j ) .< ( lastS ` d ) /\ ( lastS ` d ) .< ( lastS ` ( d ++ <" x "> ) ) ) -> ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) ) )
149 148 imp 
 |-  ( ( ( .< Po A /\ ( ( ( d ++ <" x "> ) ` j ) e. A /\ ( lastS ` d ) e. A /\ ( lastS ` ( d ++ <" x "> ) ) e. A ) ) /\ ( ( ( d ++ <" x "> ) ` j ) .< ( lastS ` d ) /\ ( lastS ` d ) .< ( lastS ` ( d ++ <" x "> ) ) ) ) -> ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) )
150 79 124 142 147 149 syl22anc 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ) -> ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) )
151 145 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> ( lastS ` d ) .< x )
152 81 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> d e. Word A )
153 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> x e. A )
154 153 s1cld 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> <" x "> e. Word A )
155 101 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> ( # ` d ) e. NN )
156 fzo0end 
 |-  ( ( # ` d ) e. NN -> ( ( # ` d ) - 1 ) e. ( 0 ..^ ( # ` d ) ) )
157 155 156 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> ( ( # ` d ) - 1 ) e. ( 0 ..^ ( # ` d ) ) )
158 ccatval1 
 |-  ( ( d e. Word A /\ <" x "> e. Word A /\ ( ( # ` d ) - 1 ) e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) = ( d ` ( ( # ` d ) - 1 ) ) )
159 152 154 157 158 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) = ( d ` ( ( # ` d ) - 1 ) ) )
160 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> j = ( ( # ` d ) - 1 ) )
161 160 fveq2d 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> ( ( d ++ <" x "> ) ` j ) = ( ( d ++ <" x "> ) ` ( ( # ` d ) - 1 ) ) )
162 lsw 
 |-  ( d e. Word A -> ( lastS ` d ) = ( d ` ( ( # ` d ) - 1 ) ) )
163 152 162 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> ( lastS ` d ) = ( d ` ( ( # ` d ) - 1 ) ) )
164 159 161 163 3eqtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> ( ( d ++ <" x "> ) ` j ) = ( lastS ` d ) )
165 121 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> ( lastS ` ( d ++ <" x "> ) ) = x )
166 151 164 165 3brtr4d 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) /\ j = ( ( # ` d ) - 1 ) ) -> ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) )
167 67 fveq2i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
168 nnuz 
 |-  NN = ( ZZ>= ` 1 )
169 167 168 eqtr4i 
 |-  ( ZZ>= ` ( 0 + 1 ) ) = NN
170 101 169 eleqtrrdi 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( # ` d ) e. ( ZZ>= ` ( 0 + 1 ) ) )
171 fzosplitsnm1 
 |-  ( ( 0 e. ZZ /\ ( # ` d ) e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( 0 ..^ ( # ` d ) ) = ( ( 0 ..^ ( ( # ` d ) - 1 ) ) u. { ( ( # ` d ) - 1 ) } ) )
172 48 170 171 sylancr 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( 0 ..^ ( # ` d ) ) = ( ( 0 ..^ ( ( # ` d ) - 1 ) ) u. { ( ( # ` d ) - 1 ) } ) )
173 133 172 eleqtrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> j e. ( ( 0 ..^ ( ( # ` d ) - 1 ) ) u. { ( ( # ` d ) - 1 ) } ) )
174 elunsn 
 |-  ( j e. ( ( 0 ..^ ( ( # ` d ) - 1 ) ) u. { ( ( # ` d ) - 1 ) } ) -> ( j e. ( ( 0 ..^ ( ( # ` d ) - 1 ) ) u. { ( ( # ` d ) - 1 ) } ) <-> ( j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) \/ j = ( ( # ` d ) - 1 ) ) ) )
175 174 ibi 
 |-  ( j e. ( ( 0 ..^ ( ( # ` d ) - 1 ) ) u. { ( ( # ` d ) - 1 ) } ) -> ( j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) \/ j = ( ( # ` d ) - 1 ) ) )
176 173 175 syl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( j e. ( 0 ..^ ( ( # ` d ) - 1 ) ) \/ j = ( ( # ` d ) - 1 ) ) )
177 150 166 176 mpjaodan 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) /\ d =/= (/) ) -> ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) )
178 78 177 pm2.61dane 
 |-  ( ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) /\ j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ) -> ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) )
179 178 ralrimiva 
 |-  ( ( ( ( ( ph /\ d e. ( .< Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .< x ) ) /\ A. i e. ( 0 ..^ ( ( # ` d ) - 1 ) ) ( d ` i ) .< ( lastS ` d ) ) -> A. j e. ( 0 ..^ ( ( # ` ( d ++ <" x "> ) ) - 1 ) ) ( ( d ++ <" x "> ) ` j ) .< ( lastS ` ( d ++ <" x "> ) ) )
180 12 19 30 37 2 58 179 chnind 
 |-  ( ph -> A. i e. ( 0 ..^ ( ( # ` C ) - 1 ) ) ( C ` i ) .< ( lastS ` C ) )
181 5 180 3 rspcdva 
 |-  ( ph -> ( C ` I ) .< ( lastS ` C ) )