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 \in {Chain}_{A} \underset{˙}{<} \to reverse (B) \in {Chain}_{A} {\underset{˙}{<}}^{-1}$

Proof

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

Metamath Proof Explorer

Theorem chnrev

Proof