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 hash0 
 |-  ( # ` (/) ) = 0
35 0nnn 
 |-  -. 0 e. NN
36 34 35 eqneltri 
 |-  -. ( # ` (/) ) e. NN
37 fzo0n0 
 |-  ( ( 0 ..^ ( # ` (/) ) ) =/= (/) <-> ( # ` (/) ) e. NN )
38 36 37 mtbir 
 |-  -. ( 0 ..^ ( # ` (/) ) ) =/= (/)
39 nne 
 |-  ( -. ( 0 ..^ ( # ` (/) ) ) =/= (/) <-> ( 0 ..^ ( # ` (/) ) ) = (/) )
40 38 39 mpbi 
 |-  ( 0 ..^ ( # ` (/) ) ) = (/)
41 rzal 
 |-  ( ( 0 ..^ ( # ` (/) ) ) = (/) -> A. i e. ( 0 ..^ ( # ` (/) ) ) ( (/) ` i ) .~ ( lastS ` (/) ) )
42 40 41 mp1i 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` (/) ) ) ( (/) ` i ) .~ ( lastS ` (/) ) )
43 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 )
44 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 )
45 43 44 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 )
46 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 ) )
47 46 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 )
48 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 "> ) ) ) )
49 ccatws1len 
 |-  ( d e. Word A -> ( # ` ( d ++ <" x "> ) ) = ( ( # ` d ) + 1 ) )
50 47 49 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 ) )
51 fveq2 
 |-  ( d = (/) -> ( # ` d ) = ( # ` (/) ) )
52 51 34 eqtr2di 
 |-  ( d = (/) -> 0 = ( # ` d ) )
53 52 eqcomd 
 |-  ( d = (/) -> ( # ` d ) = 0 )
54 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 = (/) ) -> ( # ` d ) = 0 )
55 54 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 ) )
56 0p1e1 
 |-  ( 0 + 1 ) = 1
57 55 56 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 )
58 50 57 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 )
59 58 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 ) )
60 48 59 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 ) )
61 fzo01 
 |-  ( 0 ..^ 1 ) = { 0 }
62 60 61 eleqtrdi 
 |-  ( ( ( ( ( ( ( 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 } )
63 62 elsnd 
 |-  ( ( ( ( ( ( ( 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 )
64 52 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 ) )
65 63 64 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 ) )
66 ccats1val2 
 |-  ( ( d e. Word A /\ x e. A /\ j = ( # ` d ) ) -> ( ( d ++ <" x "> ) ` j ) = x )
67 47 44 65 66 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 )
68 lswccats1 
 |-  ( ( d e. Word A /\ x e. A ) -> ( lastS ` ( d ++ <" x "> ) ) = x )
69 47 44 68 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 )
70 45 67 69 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 "> ) ) )
71 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 )
72 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 ) )
73 72 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 )
74 73 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 )
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 =/= (/) ) /\ j = ( # ` d ) ) -> x e. A )
76 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 ) )
77 74 75 76 66 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 )
78 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 ) )
79 neneq 
 |-  ( d =/= (/) -> -. d = (/) )
80 79 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 = (/) )
81 78 80 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 )
82 71 81 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 ) )
83 82 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 ) )
84 77 83 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 ) )
85 fveq2 
 |-  ( i = j -> ( ( d ++ <" x "> ) ` i ) = ( ( d ++ <" x "> ) ` j ) )
86 85 breq1d 
 |-  ( i = j -> ( ( ( d ++ <" x "> ) ` i ) .~ ( lastS ` d ) <-> ( ( d ++ <" x "> ) ` j ) .~ ( lastS ` d ) ) )
87 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 =/= (/) ) /\ j =/= ( # ` d ) ) -> A. i e. ( 0 ..^ ( # ` d ) ) ( d ` i ) .~ ( lastS ` d ) )
88 simplr 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> d e. ( .~ Chain A ) )
89 88 chnwrd 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> d e. Word A )
90 simpr 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> i e. ( 0 ..^ ( # ` d ) ) )
91 ccats1val1 
 |-  ( ( d e. Word A /\ i e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ++ <" x "> ) ` i ) = ( d ` i ) )
92 89 90 91 syl2anc 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ++ <" x "> ) ` i ) = ( d ` i ) )
93 92 eqcomd 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> ( d ` i ) = ( ( d ++ <" x "> ) ` i ) )
94 93 breq1d 
 |-  ( ( ( ph /\ d e. ( .~ Chain A ) ) /\ i e. ( 0 ..^ ( # ` d ) ) ) -> ( ( d ` i ) .~ ( lastS ` d ) <-> ( ( d ++ <" x "> ) ` i ) .~ ( lastS ` d ) ) )
95 94 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 ) ) )
96 95 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 ) ) )
97 87 96 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 ) )
98 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 "> ) ) ) )
99 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 ) )
100 99 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 )
101 100 49 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 ) )
102 101 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 ) ) )
103 98 102 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 ) ) )
104 103 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 ) ) )
105 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 ) )
106 105 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 )
107 lencl 
 |-  ( d e. Word A -> ( # ` d ) e. NN0 )
108 elnn0uz 
 |-  ( ( # ` d ) e. NN0 <-> ( # ` d ) e. ( ZZ>= ` 0 ) )
109 108 biimpi 
 |-  ( ( # ` d ) e. NN0 -> ( # ` d ) e. ( ZZ>= ` 0 ) )
110 106 107 109 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 ) )
111 fzosplitsni 
 |-  ( ( # ` d ) e. ( ZZ>= ` 0 ) -> ( j e. ( 0 ..^ ( ( # ` d ) + 1 ) ) <-> ( j e. ( 0 ..^ ( # ` d ) ) \/ j = ( # ` d ) ) ) )
112 110 111 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 ) ) ) )
113 104 112 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 ) ) )
114 df-ne 
 |-  ( j =/= ( # ` d ) <-> -. j = ( # ` d ) )
115 114 bilani 
 |-  ( ( ( ( ( ( ( ( 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 ) )
116 113 115 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 ) ) )
117 86 97 116 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 ) )
118 84 117 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 ) )
119 71 118 81 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 )
120 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 )
121 73 120 68 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 )
122 119 121 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 "> ) ) )
123 70 122 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 "> ) ) )
124 123 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 "> ) ) )
125 11 17 27 33 2 42 124 chnind 
 |-  ( ph -> A. i e. ( 0 ..^ ( # ` C ) ) ( C ` i ) .~ ( lastS ` C ) )
126 5 125 3 rspcdva 
 |-  ( ph -> ( C ` J ) .~ ( lastS ` C ) )