Metamath Proof Explorer

Theorem chnrev

Description: Reverse of a chain is chain under the converse relation and same domain. (Contributed by Ender Ting, 20-Jan-2026)

Ref Expression
Assertion chnrev 
|- ( B e. ( .< Chain A ) -> ( reverse ` B ) e. ( `' .< Chain A ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( B e. ( .< Chain A ) -> B e. ( .< Chain A ) )
2 1 chnwrd 
 |-  ( B e. ( .< Chain A ) -> B e. Word A )
3 revcl 
 |-  ( B e. Word A -> ( reverse ` B ) e. Word A )
4 2 3 syl 
 |-  ( B e. ( .< Chain A ) -> ( reverse ` B ) e. Word A )
5 simpl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> B e. ( .< Chain A ) )
6 fzossfz 
 |-  ( 0 ..^ ( # ` ( reverse ` B ) ) ) C_ ( 0 ... ( # ` ( reverse ` B ) ) )
7 6 a1i 
 |-  ( B e. ( .< Chain A ) -> ( 0 ..^ ( # ` ( reverse ` B ) ) ) C_ ( 0 ... ( # ` ( reverse ` B ) ) ) )
8 wrddm 
 |-  ( ( reverse ` B ) e. Word A -> dom ( reverse ` B ) = ( 0 ..^ ( # ` ( reverse ` B ) ) ) )
9 4 8 syl 
 |-  ( B e. ( .< Chain A ) -> dom ( reverse ` B ) = ( 0 ..^ ( # ` ( reverse ` B ) ) ) )
10 revlen 
 |-  ( B e. Word A -> ( # ` ( reverse ` B ) ) = ( # ` B ) )
11 2 10 syl 
 |-  ( B e. ( .< Chain A ) -> ( # ` ( reverse ` B ) ) = ( # ` B ) )
12 11 eqcomd 
 |-  ( B e. ( .< Chain A ) -> ( # ` B ) = ( # ` ( reverse ` B ) ) )
13 12 oveq2d 
 |-  ( B e. ( .< Chain A ) -> ( 0 ... ( # ` B ) ) = ( 0 ... ( # ` ( reverse ` B ) ) ) )
14 7 9 13 3sstr4d 
 |-  ( B e. ( .< Chain A ) -> dom ( reverse ` B ) C_ ( 0 ... ( # ` B ) ) )
15 14 ssdifd 
 |-  ( B e. ( .< Chain A ) -> ( dom ( reverse ` B ) \ { 0 } ) C_ ( ( 0 ... ( # ` B ) ) \ { 0 } ) )
16 15 sselda 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n e. ( ( 0 ... ( # ` B ) ) \ { 0 } ) )
17 2 adantr 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> B e. Word A )
18 lencl 
 |-  ( B e. Word A -> ( # ` B ) e. NN0 )
19 17 18 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( # ` B ) e. NN0 )
20 fz0dif1 
 |-  ( ( # ` B ) e. NN0 -> ( ( 0 ... ( # ` B ) ) \ { 0 } ) = ( 1 ... ( # ` B ) ) )
21 19 20 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( 0 ... ( # ` B ) ) \ { 0 } ) = ( 1 ... ( # ` B ) ) )
22 16 21 eleqtrd 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n e. ( 1 ... ( # ` B ) ) )
23 ubmelfzo 
 |-  ( n e. ( 1 ... ( # ` B ) ) -> ( ( # ` B ) - n ) e. ( 0 ..^ ( # ` B ) ) )
24 22 23 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( # ` B ) - n ) e. ( 0 ..^ ( # ` B ) ) )
25 wrddm 
 |-  ( B e. Word A -> dom B = ( 0 ..^ ( # ` B ) ) )
26 17 25 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> dom B = ( 0 ..^ ( # ` B ) ) )
27 24 26 eleqtrrd 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( # ` B ) - n ) e. dom B )
28 19 nn0cnd 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( # ` B ) e. CC )
29 eldifi 
 |-  ( n e. ( dom ( reverse ` B ) \ { 0 } ) -> n e. dom ( reverse ` B ) )
30 29 anim2i 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( B e. ( .< Chain A ) /\ n e. dom ( reverse ` B ) ) )
31 2 3 8 3syl 
 |-  ( B e. ( .< Chain A ) -> dom ( reverse ` B ) = ( 0 ..^ ( # ` ( reverse ` B ) ) ) )
32 31 eleq2d 
 |-  ( B e. ( .< Chain A ) -> ( n e. dom ( reverse ` B ) <-> n e. ( 0 ..^ ( # ` ( reverse ` B ) ) ) ) )
33 32 biimpa 
 |-  ( ( B e. ( .< Chain A ) /\ n e. dom ( reverse ` B ) ) -> n e. ( 0 ..^ ( # ` ( reverse ` B ) ) ) )
34 elfzoelz 
 |-  ( n e. ( 0 ..^ ( # ` ( reverse ` B ) ) ) -> n e. ZZ )
35 33 34 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. dom ( reverse ` B ) ) -> n e. ZZ )
36 zcn 
 |-  ( n e. ZZ -> n e. CC )
37 30 35 36 3syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n e. CC )
38 29 adantl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n e. dom ( reverse ` B ) )
39 17 3 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( reverse ` B ) e. Word A )
40 wrdlndm 
 |-  ( ( reverse ` B ) e. Word A -> ( # ` ( reverse ` B ) ) e/ dom ( reverse ` B ) )
41 39 40 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( # ` ( reverse ` B ) ) e/ dom ( reverse ` B ) )
42 17 10 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( # ` ( reverse ` B ) ) = ( # ` B ) )
43 eqidd 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> dom ( reverse ` B ) = dom ( reverse ` B ) )
44 42 43 neleq12d 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( # ` ( reverse ` B ) ) e/ dom ( reverse ` B ) <-> ( # ` B ) e/ dom ( reverse ` B ) ) )
45 41 44 mpbid 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( # ` B ) e/ dom ( reverse ` B ) )
46 elnelne2 
 |-  ( ( n e. dom ( reverse ` B ) /\ ( # ` B ) e/ dom ( reverse ` B ) ) -> n =/= ( # ` B ) )
47 38 45 46 syl2anc 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n =/= ( # ` B ) )
48 47 necomd 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( # ` B ) =/= n )
49 28 37 48 subne0d 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( # ` B ) - n ) =/= 0 )
50 27 49 eldifsnd 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( # ` B ) - n ) e. ( dom B \ { 0 } ) )
51 5 50 chnltm1 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( B ` ( ( ( # ` B ) - n ) - 1 ) ) .< ( B ` ( ( # ` B ) - n ) ) )
52 1cnd 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> 1 e. CC )
53 28 52 37 sub32d 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( ( # ` B ) - 1 ) - n ) = ( ( ( # ` B ) - n ) - 1 ) )
54 53 fveq2d 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( B ` ( ( ( # ` B ) - 1 ) - n ) ) = ( B ` ( ( ( # ` B ) - n ) - 1 ) ) )
55 28 37 52 nnncan2d 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( ( # ` B ) - 1 ) - ( n - 1 ) ) = ( ( # ` B ) - n ) )
56 55 fveq2d 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( B ` ( ( ( # ` B ) - 1 ) - ( n - 1 ) ) ) = ( B ` ( ( # ` B ) - n ) ) )
57 51 54 56 3brtr4d 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( B ` ( ( ( # ` B ) - 1 ) - n ) ) .< ( B ` ( ( ( # ` B ) - 1 ) - ( n - 1 ) ) ) )
58 fvex 
 |-  ( B ` ( ( ( # ` B ) - 1 ) - ( n - 1 ) ) ) e. _V
59 fvex 
 |-  ( B ` ( ( ( # ` B ) - 1 ) - n ) ) e. _V
60 58 59 brcnv 
 |-  ( ( B ` ( ( ( # ` B ) - 1 ) - ( n - 1 ) ) ) `' .< ( B ` ( ( ( # ` B ) - 1 ) - n ) ) <-> ( B ` ( ( ( # ` B ) - 1 ) - n ) ) .< ( B ` ( ( ( # ` B ) - 1 ) - ( n - 1 ) ) ) )
61 57 60 sylibr 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( B ` ( ( ( # ` B ) - 1 ) - ( n - 1 ) ) ) `' .< ( B ` ( ( ( # ` B ) - 1 ) - n ) ) )
62 39 8 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> dom ( reverse ` B ) = ( 0 ..^ ( # ` ( reverse ` B ) ) ) )
63 38 62 eleqtrd 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n e. ( 0 ..^ ( # ` ( reverse ` B ) ) ) )
64 elfzonn0 
 |-  ( n e. ( 0 ..^ ( # ` ( reverse ` B ) ) ) -> n e. NN0 )
65 63 64 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n e. NN0 )
66 eldifsni 
 |-  ( n e. ( dom ( reverse ` B ) \ { 0 } ) -> n =/= 0 )
67 66 adantl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n =/= 0 )
68 elnnne0 
 |-  ( n e. NN <-> ( n e. NN0 /\ n =/= 0 ) )
69 65 67 68 sylanbrc 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n e. NN )
70 nnm1nn0 
 |-  ( n e. NN -> ( n - 1 ) e. NN0 )
71 69 70 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( n - 1 ) e. NN0 )
72 elfzo0le 
 |-  ( n e. ( 0 ..^ ( # ` ( reverse ` B ) ) ) -> n <_ ( # ` ( reverse ` B ) ) )
73 63 72 syl 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n <_ ( # ` ( reverse ` B ) ) )
74 37 52 npcand 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( n - 1 ) + 1 ) = n )
75 42 eqcomd 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( # ` B ) = ( # ` ( reverse ` B ) ) )
76 73 74 75 3brtr4d 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( n - 1 ) + 1 ) <_ ( # ` B ) )
77 nn0p1elfzo 
 |-  ( ( ( n - 1 ) e. NN0 /\ ( # ` B ) e. NN0 /\ ( ( n - 1 ) + 1 ) <_ ( # ` B ) ) -> ( n - 1 ) e. ( 0 ..^ ( # ` B ) ) )
78 71 19 76 77 syl3anc 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( n - 1 ) e. ( 0 ..^ ( # ` B ) ) )
79 revfv 
 |-  ( ( B e. Word A /\ ( n - 1 ) e. ( 0 ..^ ( # ` B ) ) ) -> ( ( reverse ` B ) ` ( n - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - ( n - 1 ) ) ) )
80 17 78 79 syl2anc 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( reverse ` B ) ` ( n - 1 ) ) = ( B ` ( ( ( # ` B ) - 1 ) - ( n - 1 ) ) ) )
81 11 oveq2d 
 |-  ( B e. ( .< Chain A ) -> ( 0 ..^ ( # ` ( reverse ` B ) ) ) = ( 0 ..^ ( # ` B ) ) )
82 31 81 eqtrd 
 |-  ( B e. ( .< Chain A ) -> dom ( reverse ` B ) = ( 0 ..^ ( # ` B ) ) )
83 82 eleq2d 
 |-  ( B e. ( .< Chain A ) -> ( n e. dom ( reverse ` B ) <-> n e. ( 0 ..^ ( # ` B ) ) ) )
84 29 83 imbitrid 
 |-  ( B e. ( .< Chain A ) -> ( n e. ( dom ( reverse ` B ) \ { 0 } ) -> n e. ( 0 ..^ ( # ` B ) ) ) )
85 84 imp 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> n e. ( 0 ..^ ( # ` B ) ) )
86 revfv 
 |-  ( ( B e. Word A /\ n e. ( 0 ..^ ( # ` B ) ) ) -> ( ( reverse ` B ) ` n ) = ( B ` ( ( ( # ` B ) - 1 ) - n ) ) )
87 17 85 86 syl2anc 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( reverse ` B ) ` n ) = ( B ` ( ( ( # ` B ) - 1 ) - n ) ) )
88 61 80 87 3brtr4d 
 |-  ( ( B e. ( .< Chain A ) /\ n e. ( dom ( reverse ` B ) \ { 0 } ) ) -> ( ( reverse ` B ) ` ( n - 1 ) ) `' .< ( ( reverse ` B ) ` n ) )
89 88 ralrimiva 
 |-  ( B e. ( .< Chain A ) -> A. n e. ( dom ( reverse ` B ) \ { 0 } ) ( ( reverse ` B ) ` ( n - 1 ) ) `' .< ( ( reverse ` B ) ` n ) )
90 ischn 
 |-  ( ( reverse ` B ) e. ( `' .< Chain A ) <-> ( ( reverse ` B ) e. Word A /\ A. n e. ( dom ( reverse ` B ) \ { 0 } ) ( ( reverse ` B ) ` ( n - 1 ) ) `' .< ( ( reverse ` B ) ` n ) ) )
91 4 89 90 sylanbrc 
 |-  ( B e. ( .< Chain A ) -> ( reverse ` B ) e. ( `' .< Chain A ) )