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 ( 𝐵 ∈ ( < Chain 𝐴 ) → ( reverse ‘ 𝐵 ) ∈ ( ◡ < Chain 𝐴 ) )

Proof

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