Metamath Proof Explorer

Theorem chnerlem1

Description: In a chain constructed on an equivalence relation, the last element is equivalent to any. This theorem is a translation of chnub to equivalence relations. (Contributed by Ender Ting, 29-Jan-2026)

Ref Expression
Hypotheses chner.1 
|- ( ph -> .~ Er A )
chner.2 
|- ( ph -> C e. ( .~ Chain A ) )
chner.3 
|- ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
Assertion chnerlem1 
|- ( ph -> ( C ` J ) .~ ( lastS ` C ) )

Proof

Step Hyp Ref Expression
1 chner.1 
 |-  ( ph -> .~ Er A )
2 chner.2 
 |-  ( ph -> C e. ( .~ Chain A ) )
3 chner.3 
 |-  ( ph -> J e. ( 0 ..^ ( # ` C ) ) )
4 fveq2 
 |-  ( i = J -> ( C ` i ) = ( C ` J ) )
5 4 breq1d 
 |-  ( i = J -> ( ( C ` i ) .~ ( lastS ` C ) <-> ( C ` J ) .~ ( lastS ` C ) ) )
6 fveq2 
 |-  ( c = (/) -> ( # ` c ) = ( # ` (/) ) )
7 6 oveq2d 
 |-  ( c = (/) -> ( 0 ..^ ( # ` c ) ) = ( 0 ..^ ( # ` (/) ) ) )
8 fveq1 
 |-  ( c = (/) -> ( c ` i ) = ( (/) ` i ) )
9 fveq2 
 |-  ( c = (/) -> ( lastS ` c ) = ( lastS ` (/) ) )
10 8 9 breq12d 
 |-  ( c = (/) -> ( ( c ` i ) .~ ( lastS ` c ) <-> ( (/) ` i ) .~ ( lastS ` (/) ) ) )
11 7 10 raleqbidv 
 |-  ( c = (/) -> ( A. i e. ( 0 ..^ ( # ` c ) ) ( c ` i ) .~ ( lastS ` c ) <-> A. i e. ( 0 ..^ ( # ` (/) ) ) ( (/) ` i ) .~ ( lastS ` (/) ) ) )
12 fveq2 
 |-  ( c = d -> ( # ` c ) = ( # ` d ) )
13 12 oveq2d 
 |-  ( c = d -> ( 0 ..^ ( # ` c ) ) = ( 0 ..^ ( # ` d ) ) )
14 fveq1 
 |-  ( c = d -> ( c ` i ) = ( d ` i ) )
15 fveq2 
 |-  ( c = d -> ( lastS ` c ) = ( lastS ` d ) )
16 14 15 breq12d 
 |-  ( c = d -> ( ( c ` i ) .~ ( lastS ` c ) <-> ( d ` i ) .~ ( lastS ` d ) ) )
17 13 16 raleqbidv 
 |-  ( c = d -> ( A. i e. ( 0 ..^ ( # ` c ) ) ( c ` i ) .~ ( lastS ` c ) <-> A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) )
18 fveq2 
 |-  ( i = j -> ( c ` i ) = ( c ` j ) )
19 18 breq1d 
 |-  ( i = j -> ( ( c ` i ) .~ ( lastS ` c ) <-> ( c ` j ) .~ ( lastS ` c ) ) )
20 19 cbvralvw 
 |-  ( A. i e. ( 0 ..^ ( # ` c ) ) ( c ` i ) .~ ( lastS ` c ) <-> A. j e. ( 0 ..^ ( # ` c ) ) ( c ` j ) .~ ( lastS ` c ) )
21 fveq2 
 |-  ( c = ( d ++ <" x "> ) -> ( # ` c ) = ( # ` ( d ++ <" x "> ) ) )
22 21 oveq2d 
 |-  ( c = ( d ++ <" x "> ) -> ( 0 ..^ ( # ` c ) ) = ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) )
23 fveq1 
 |-  ( c = ( d ++ <" x "> ) -> ( c ` j ) = ( ( d ++ <" x "> ) ` j ) )
24 fveq2 
 |-  ( c = ( d ++ <" x "> ) -> ( lastS ` c ) = ( lastS ` ( d ++ <" x "> ) ) )
25 23 24 breq12d 
 |-  ( c = ( d ++ <" x "> ) -> ( ( c ` j ) .~ ( lastS ` c ) <-> ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` ( d ++ <" x "> ) ) ) )
26 22 25 raleqbidv 
 |-  ( c = ( d ++ <" x "> ) -> ( A. j e. ( 0 ..^ ( # ` c ) ) ( c ` j ) .~ ( lastS ` c ) <-> A. j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` ( d ++ <" x "> ) ) ) )
27 20 26 bitrid 
 |-  ( c = ( d ++ <" x "> ) -> ( A. i e. ( 0 ..^ ( # ` c ) ) ( c ` i ) .~ ( lastS ` c ) <-> A. j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` ( d ++ <" x "> ) ) ) )
28 fveq2 
 |-  ( c = C -> ( # ` c ) = ( # ` C ) )
29 28 oveq2d 
 |-  ( c = C -> ( 0 ..^ ( # ` c ) ) = ( 0 ..^ ( # ` C ) ) )
30 fveq1 
 |-  ( c = C -> ( c ` i ) = ( C ` i ) )
31 fveq2 
 |-  ( c = C -> ( lastS ` c ) = ( lastS ` C ) )
32 30 31 breq12d 
 |-  ( c = C -> ( ( c ` i ) .~ ( lastS ` c ) <-> ( C ` i ) .~ ( lastS ` C ) ) )
33 29 32 raleqbidv 
 |-  ( c = C -> ( A. i e. ( 0 ..^ ( # ` c ) ) ( c ` i ) .~ ( lastS ` c ) <-> A. i e. ( 0 ..^ ( # ` C ) ) ( C ` i ) .~ ( lastS ` C ) ) )
34 0nnn 
 |-  -. 0 e. NN
35 hash0 
 |-  ( # ` (/) ) = 0
36 35 eleq1i 
 |-  ( ( # ` (/) ) e. NN <-> 0 e. NN )
37 34 36 mtbir 
 |-  -. ( # ` (/) ) e. NN
38 fzo0n0 
 |-  ( ( 0 ..^ ( # ` (/) ) ) =/= (/) <-> ( # ` (/) ) e. NN )
39 37 38 mtbir 
 |-  -. ( 0 ..^ ( # ` (/) ) ) =/= (/)
40 nne 
 |-  ( -. ( 0 ..^ ( # ` (/) ) ) =/= (/) <-> ( 0 ..^ ( # ` (/) ) ) = (/) )
41 39 40 mpbi 
 |-  ( 0 ..^ ( # ` (/) ) ) = (/)
42 rzal 
 |-  ( ( 0 ..^ ( # ` (/) ) ) = (/) -> A. i e. ( 0 ..^ ( # ` (/) ) ) ( (/) ` i ) .~ ( lastS ` (/) ) )
43 41 42 mp1i 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` (/) ) ) ( (/) ` i ) .~ ( lastS ` (/) ) )
44 1 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> .~ Er A )
45 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> x e. A )
46 44 45 erref 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> x .~ x )
47 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> d e. ( .~ Chain A ) )
48 47 chnwrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> d e. Word A )
49 simplr 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) )
50 ccatws1len 
 |-  ( d e. Word A -> ( # ` ( d ++ <" x "> ) ) = ( ( # ` d ) + 1 ) )
51 48 50 syl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( # ` ( d ++ <" x "> ) ) = ( ( # ` d ) + 1 ) )
52 fveq2 
 |-  ( d = (/) -> ( # ` d ) = ( # ` (/) ) )
53 52 35 eqtr2di 
 |-  ( d = (/) -> 0 = ( # ` d ) )
54 53 eqcomd 
 |-  ( d = (/) -> ( # ` d ) = 0 )
55 54 adantl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( # ` d ) = 0 )
56 55 oveq1d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( ( # ` d ) + 1 ) = ( 0 + 1 ) )
57 0p1e1 
 |-  ( 0 + 1 ) = 1
58 56 57 eqtrdi 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( ( # ` d ) + 1 ) = 1 )
59 51 58 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( # ` ( d ++ <" x "> ) ) = 1 )
60 59 oveq2d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) = ( 0 ..^ 1 ) )
61 49 60 eleqtrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> j e. ( 0 ..^ 1 ) )
62 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
63 62 a1i 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( 0 ..^ 1 ) = { 0 } )
64 61 63 eleqtrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> j e. { 0 } )
65 elsni 
 |-  ( j e. { 0 } -> j = 0 )
66 64 65 syl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> j = 0 )
67 53 adantl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> 0 = ( # ` d ) )
68 66 67 eqtrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> j = ( # ` d ) )
69 ccats1val2 
 |-  ( ( d e. Word A /\ x e. A /\ j = ( # ` d ) ) -> ( ( d ++ <" x "> ) ` j ) = x )
70 48 45 68 69 syl3anc 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( ( d ++ <" x "> ) ` j ) = x )
71 lswccats1 
 |-  ( ( d e. Word A /\ x e. A ) -> ( lastS ` ( d ++ <" x "> ) ) = x )
72 48 45 71 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( lastS ` ( d ++ <" x "> ) ) = x )
73 46 70 72 3brtr4d 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d = (/) ) -> ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` ( d ++ <" x "> ) ) )
74 1 ad6antr 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> .~ Er A )
75 simp-6r 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> d e. ( .~ Chain A ) )
76 75 chnwrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> d e. Word A )
77 76 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j = ( # ` d ) ) -> d e. Word A )
78 simp-6r 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j = ( # ` d ) ) -> x e. A )
79 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j = ( # ` d ) ) -> j = ( # ` d ) )
80 77 78 79 69 syl3anc 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j = ( # ` d ) ) -> ( ( d ++ <" x "> ) ` j ) = x )
81 simp-4r 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> ( d = (/) \/ ( lastS ` d ) .~ x ) )
82 neneq 
 |-  ( d =/= (/) -> -. d = (/) )
83 82 adantl 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> -. d = (/) )
84 81 83 orcnd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> ( lastS ` d ) .~ x )
85 74 84 ersym 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> x .~ ( lastS ` d ) )
86 85 adantr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j = ( # ` d ) ) -> x .~ ( lastS ` d ) )
87 80 86 eqbrtrd 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j = ( # ` d ) ) -> ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` d ) )
88 fveq2 
 |-  ( i = j -> ( ( d ++ <" x "> ) ` i ) = ( ( d ++ <" x "> ) ` j ) )
89 88 breq1d 
 |-  ( i = j -> ( ( ( d ++ <" x "> ) ` i ) .~ ( lastS ` d ) <-> ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` d ) ) )
90 simpr 
 |-  ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) -> A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) )
91 90 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) )
92 simplr 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> d e. ( .~ Chain A ) )
93 92 chnwrd 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> d e. Word A )
94 simpr 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> i e. ( 0 ..^ ( # ` d ) ) )
95 ccats1val1 
 |-  ( ( d e. Word A /\ i e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ++ <" x "> ) ` i ) = ( d ` i ) )
96 93 94 95 syl2anc 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ++ <" x "> ) ` i ) = ( d ` i ) )
97 96 eqcomd 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> ( d ` i ) = ( ( d ++ <" x "> ) ` i ) )
98 97 breq1d 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ` i ) .~ ( lastS ` d ) <-> ( ( d ++ <" x "> ) ` i ) .~ ( lastS ` d ) ) )
99 98 ralbidva 
 |-  ( ( ph /\ d e. ( .~ Chain A ) ) -> ( A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) <-> A. i e. ( 0 ..^ ( # ` d ) ) ( ( d ++ <" x "> ) ` i ) .~ ( lastS ` d ) ) )
100 99 ad6antr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> ( A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) <-> A. i e. ( 0 ..^ ( # ` d ) ) ( ( d ++ <" x "> ) ` i ) .~ ( lastS ` d ) ) )
101 91 100 mpbid 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> A. i e. ( 0 ..^ ( # ` d ) ) ( ( d ++ <" x "> ) ` i ) .~ ( lastS ` d ) )
102 simpr 
 |-  ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) -> j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) )
103 simp-5r 
 |-  ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) -> d e. ( .~ Chain A ) )
104 103 chnwrd 
 |-  ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) -> d e. Word A )
105 104 50 syl 
 |-  ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) -> ( # ` ( d ++ <" x "> ) ) = ( ( # ` d ) + 1 ) )
106 105 oveq2d 
 |-  ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) -> ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) = ( 0 ..^ ( ( # ` d ) + 1 ) ) )
107 102 106 eleqtrd 
 |-  ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) -> j e. ( 0 ..^ ( ( # ` d ) + 1 ) ) )
108 107 ad2antrr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> j e. ( 0 ..^ ( ( # ` d ) + 1 ) ) )
109 simp-7r 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> d e. ( .~ Chain A ) )
110 109 chnwrd 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> d e. Word A )
111 lencl 
 |-  ( d e. Word A -> ( # ` d ) e. NN0 )
112 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
113 112 eleq2i 
 |-  ( ( # ` d ) e. NN0 <-> ( # ` d ) e. ( ZZ>= ` 0 ) )
114 113 biimpi 
 |-  ( ( # ` d ) e. NN0 -> ( # ` d ) e. ( ZZ>= ` 0 ) )
115 110 111 114 3syl 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> ( # ` d ) e. ( ZZ>= ` 0 ) )
116 fzosplitsni 
 |-  ( ( # ` d ) e. ( ZZ>= ` 0 ) -> ( j e. ( 0 ..^ ( ( # ` d ) + 1 ) ) <-> ( j e. ( 0 ..^ ( # ` d ) ) \/ j = ( # ` d ) ) ) )
117 115 116 syl 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> ( j e. ( 0 ..^ ( ( # ` d ) + 1 ) ) <-> ( j e. ( 0 ..^ ( # ` d ) ) \/ j = ( # ` d ) ) ) )
118 108 117 mpbid 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> ( j e. ( 0 ..^ ( # ` d ) ) \/ j = ( # ` d ) ) )
119 simpr 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> j =/= ( # ` d ) )
120 df-ne 
 |-  ( j =/= ( # ` d ) <-> -. j = ( # ` d ) )
121 119 120 sylib 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> -. j = ( # ` d ) )
122 118 121 olcnd 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> j e. ( 0 ..^ ( # ` d ) ) )
123 89 101 122 rspcdva 
 |-  ( ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) /\ j =/= ( # ` d ) ) -> ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` d ) )
124 87 123 pm2.61dane 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` d ) )
125 74 124 84 ertrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> ( ( d ++ <" x "> ) ` j ) .~ x )
126 simp-5r 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> x e. A )
127 76 126 71 syl2anc 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> ( lastS ` ( d ++ <" x "> ) ) = x )
128 125 127 breqtrrd 
 |-  ( ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) /\ d =/= (/) ) -> ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` ( d ++ <" x "> ) ) )
129 73 128 pm2.61dane 
 |-  ( ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) /\ j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ) -> ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` ( d ++ <" x "> ) ) )
130 129 ralrimiva 
 |-  ( ( ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ x e. A ) /\ ( d = (/) \/ ( lastS ` d ) .~ x ) ) /\ A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) ) -> A. j e. ( 0 ..^ ( # ` ( d ++ <" x "> ) ) ) ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` ( d ++ <" x "> ) ) )
131 11 17 27 33 2 43 130 chnind 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` C ) ) ( C ` i ) .~ ( lastS ` C ) )
132 5 131 3 rspcdva 
 |-  ( ph -> ( C ` J ) .~ ( lastS ` C ) )