chnrev - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > chnrev		Structured version Visualization version GIF version

Theorem chnrev 18682

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

**Assertion**
Ref	Expression
chnrev	⊢ (𝐵 ∈ ( < Chain 𝐴) → (reverse‘𝐵) ∈ (^◡ < Chain 𝐴))

Proof of Theorem chnrev Dummy variable 𝑛 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 23	. . . 4 ⊢ (𝐵 ∈ ( < Chain 𝐴) → 𝐵 ∈ ( < Chain 𝐴))
2	1	chnwrd 18663	. . 3 ⊢ (𝐵 ∈ ( < Chain 𝐴) → 𝐵 ∈ Word 𝐴)
3		revcl 14797	. . 3 ⊢ (𝐵 ∈ Word 𝐴 → (reverse‘𝐵) ∈ Word 𝐴)
4	2, 3	syl 18	. 2 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (reverse‘𝐵) ∈ Word 𝐴)
5		simpl 487	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝐵 ∈ ( < Chain 𝐴))
6		fzossfz 13706	. . . . . . . . . . . . . . 15 ⊢ (0..^(♯‘(reverse‘𝐵))) ⊆ (0...(♯‘(reverse‘𝐵)))
7	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (0..^(♯‘(reverse‘𝐵))) ⊆ (0...(♯‘(reverse‘𝐵))))
8		wrddm 14557	. . . . . . . . . . . . . . 15 ⊢ ((reverse‘𝐵) ∈ Word 𝐴 → dom (reverse‘𝐵) = (0..^(♯‘(reverse‘𝐵))))
9	4, 8	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ( < Chain 𝐴) → dom (reverse‘𝐵) = (0..^(♯‘(reverse‘𝐵))))
10		revlen 14798	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ Word 𝐴 → (♯‘(reverse‘𝐵)) = (♯‘𝐵))
11	2, 10	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (♯‘(reverse‘𝐵)) = (♯‘𝐵))
12	11	eqcomd 2767	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (♯‘𝐵) = (♯‘(reverse‘𝐵)))
13	12	oveq2d 7426	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (0...(♯‘𝐵)) = (0...(♯‘(reverse‘𝐵))))
14	7, 9, 13	3sstr4d 3991	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ( < Chain 𝐴) → dom (reverse‘𝐵) ⊆ (0...(♯‘𝐵)))
15	14	ssdifd 4098	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (dom (reverse‘𝐵) ∖ {0}) ⊆ ((0...(♯‘𝐵)) ∖ {0}))
16	15	sselda 3936	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ ((0...(♯‘𝐵)) ∖ {0}))
17	2	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝐵 ∈ Word 𝐴)
18		lencl 14569	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Word 𝐴 → (♯‘𝐵) ∈ ℕ₀)
19	17, 18	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) ∈ ℕ₀)
20		fz0dif1 13633	. . . . . . . . . . . 12 ⊢ ((♯‘𝐵) ∈ ℕ₀ → ((0...(♯‘𝐵)) ∖ {0}) = (1...(♯‘𝐵)))
21	19, 20	syl 18	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((0...(♯‘𝐵)) ∖ {0}) = (1...(♯‘𝐵)))
22	16, 21	eleqtrd 2863	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ (1...(♯‘𝐵)))
23		ubmelfzo 13758	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(♯‘𝐵)) → ((♯‘𝐵) − 𝑛) ∈ (0..^(♯‘𝐵)))
24	22, 23	syl 18	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘𝐵) − 𝑛) ∈ (0..^(♯‘𝐵)))
25		wrddm 14557	. . . . . . . . . 10 ⊢ (𝐵 ∈ Word 𝐴 → dom 𝐵 = (0..^(♯‘𝐵)))
26	17, 25	syl 18	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → dom 𝐵 = (0..^(♯‘𝐵)))
27	24, 26	eleqtrrd 2864	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘𝐵) − 𝑛) ∈ dom 𝐵)
28	19	nn0cnd 12566	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) ∈ ℂ)
29		eldifi 4084	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (dom (reverse‘𝐵) ∖ {0}) → 𝑛 ∈ dom (reverse‘𝐵))
30	29	anim2i 628	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ dom (reverse‘𝐵)))
31	2, 3, 8	3syl 19	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ( < Chain 𝐴) → dom (reverse‘𝐵) = (0..^(♯‘(reverse‘𝐵))))
32	31	eleq2d 2847	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (𝑛 ∈ dom (reverse‘𝐵) ↔ 𝑛 ∈ (0..^(♯‘(reverse‘𝐵)))))
33	32	biimpa 481	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ dom (reverse‘𝐵)) → 𝑛 ∈ (0..^(♯‘(reverse‘𝐵))))
34		elfzoelz 13686	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (0..^(♯‘(reverse‘𝐵))) → 𝑛 ∈ ℤ)
35	33, 34	syl 18	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ dom (reverse‘𝐵)) → 𝑛 ∈ ℤ)
36		zcn 12595	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
37	30, 35, 36	3syl 19	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ ℂ)
38	29	adantl 486	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ dom (reverse‘𝐵))
39	17, 3	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (reverse‘𝐵) ∈ Word 𝐴)
40		wrdlndm 14566	. . . . . . . . . . . . 13 ⊢ ((reverse‘𝐵) ∈ Word 𝐴 → (♯‘(reverse‘𝐵)) ∉ dom (reverse‘𝐵))
41	39, 40	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘(reverse‘𝐵)) ∉ dom (reverse‘𝐵))
42	17, 10	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘(reverse‘𝐵)) = (♯‘𝐵))
43		eqidd 2762	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → dom (reverse‘𝐵) = dom (reverse‘𝐵))
44	42, 43	neleq12d 3067	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘(reverse‘𝐵)) ∉ dom (reverse‘𝐵) ↔ (♯‘𝐵) ∉ dom (reverse‘𝐵)))
45	41, 44	mpbid 235	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) ∉ dom (reverse‘𝐵))
46		elnelne2 3074	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ dom (reverse‘𝐵) ∧ (♯‘𝐵) ∉ dom (reverse‘𝐵)) → 𝑛 ≠ (♯‘𝐵))
47	38, 45, 46	syl2anc 595	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ≠ (♯‘𝐵))
48	47	necomd 3011	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) ≠ 𝑛)
49	28, 37, 48	subne0d 11577	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘𝐵) − 𝑛) ≠ 0)
50	27, 49	eldifsnd 4754	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘𝐵) − 𝑛) ∈ (dom 𝐵 ∖ {0}))
51	5, 50	chnltm1 18664	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 𝑛) − 1)) < (𝐵‘((♯‘𝐵) − 𝑛)))
52		1cnd 11201	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 1 ∈ ℂ)
53	28, 52, 37	sub32d 11600	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (((♯‘𝐵) − 1) − 𝑛) = (((♯‘𝐵) − 𝑛) − 1))
54	53	fveq2d 6885	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) = (𝐵‘(((♯‘𝐵) − 𝑛) − 1)))
55	28, 37, 52	nnncan2d 11603	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (((♯‘𝐵) − 1) − (𝑛 − 1)) = ((♯‘𝐵) − 𝑛))
56	55	fveq2d 6885	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))) = (𝐵‘((♯‘𝐵) − 𝑛)))
57	51, 54, 56	3brtr4d 5142	. . . . 5 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) < (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))))
58		fvex 6894	. . . . . 6 ⊢ (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))) ∈ V
59		fvex 6894	. . . . . 6 ⊢ (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) ∈ V
60	58, 59	brcnv 5868	. . . . 5 ⊢ ((𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1)))^◡ < (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) ↔ (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) < (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))))
61	57, 60	sylibr 237	. . . 4 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1)))^◡ < (𝐵‘(((♯‘𝐵) − 1) − 𝑛)))
62	39, 8	syl 18	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → dom (reverse‘𝐵) = (0..^(♯‘(reverse‘𝐵))))
63	38, 62	eleqtrd 2863	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ (0..^(♯‘(reverse‘𝐵))))
64		elfzonn0 13735	. . . . . . . . 9 ⊢ (𝑛 ∈ (0..^(♯‘(reverse‘𝐵))) → 𝑛 ∈ ℕ₀)
65	63, 64	syl 18	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ ℕ₀)
66		eldifsni 4757	. . . . . . . . 9 ⊢ (𝑛 ∈ (dom (reverse‘𝐵) ∖ {0}) → 𝑛 ≠ 0)
67	66	adantl 486	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ≠ 0)
68		elnnne0 12517	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℕ₀ ∧ 𝑛 ≠ 0))
69	65, 67, 68	sylanbrc 594	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ ℕ)
70		nnm1nn0 12544	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ₀)
71	69, 70	syl 18	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝑛 − 1) ∈ ℕ₀)
72		elfzo0le 13731	. . . . . . . 8 ⊢ (𝑛 ∈ (0..^(♯‘(reverse‘𝐵))) → 𝑛 ≤ (♯‘(reverse‘𝐵)))
73	63, 72	syl 18	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ≤ (♯‘(reverse‘𝐵)))
74	37, 52	npcand 11572	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((𝑛 − 1) + 1) = 𝑛)
75	42	eqcomd 2767	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) = (♯‘(reverse‘𝐵)))
76	73, 74, 75	3brtr4d 5142	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((𝑛 − 1) + 1) ≤ (♯‘𝐵))
77		nn0p1elfzo 13730	. . . . . 6 ⊢ (((𝑛 − 1) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ ((𝑛 − 1) + 1) ≤ (♯‘𝐵)) → (𝑛 − 1) ∈ (0..^(♯‘𝐵)))
78	71, 19, 76, 77	syl3anc 1396	. . . . 5 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝑛 − 1) ∈ (0..^(♯‘𝐵)))
79		revfv 14799	. . . . 5 ⊢ ((𝐵 ∈ Word 𝐴 ∧ (𝑛 − 1) ∈ (0..^(♯‘𝐵))) → ((reverse‘𝐵)‘(𝑛 − 1)) = (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))))
80	17, 78, 79	syl2anc 595	. . . 4 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((reverse‘𝐵)‘(𝑛 − 1)) = (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))))
81	11	oveq2d 7426	. . . . . . . . 9 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (0..^(♯‘(reverse‘𝐵))) = (0..^(♯‘𝐵)))
82	31, 81	eqtrd 2796	. . . . . . . 8 ⊢ (𝐵 ∈ ( < Chain 𝐴) → dom (reverse‘𝐵) = (0..^(♯‘𝐵)))
83	82	eleq2d 2847	. . . . . . 7 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (𝑛 ∈ dom (reverse‘𝐵) ↔ 𝑛 ∈ (0..^(♯‘𝐵))))
84	29, 83	imbitrid 247	. . . . . 6 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (𝑛 ∈ (dom (reverse‘𝐵) ∖ {0}) → 𝑛 ∈ (0..^(♯‘𝐵))))
85	84	imp 411	. . . . 5 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ (0..^(♯‘𝐵)))
86		revfv 14799	. . . . 5 ⊢ ((𝐵 ∈ Word 𝐴 ∧ 𝑛 ∈ (0..^(♯‘𝐵))) → ((reverse‘𝐵)‘𝑛) = (𝐵‘(((♯‘𝐵) − 1) − 𝑛)))
87	17, 85, 86	syl2anc 595	. . . 4 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((reverse‘𝐵)‘𝑛) = (𝐵‘(((♯‘𝐵) − 1) − 𝑛)))
88	61, 80, 87	3brtr4d 5142	. . 3 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((reverse‘𝐵)‘(𝑛 − 1))^◡ < ((reverse‘𝐵)‘𝑛))
89	88	ralrimiva 3155	. 2 ⊢ (𝐵 ∈ ( < Chain 𝐴) → ∀𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})((reverse‘𝐵)‘(𝑛 − 1))^◡ < ((reverse‘𝐵)‘𝑛))
90		ischn 18662	. 2 ⊢ ((reverse‘𝐵) ∈ (^◡ < Chain 𝐴) ↔ ((reverse‘𝐵) ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})((reverse‘𝐵)‘(𝑛 − 1))^◡ < ((reverse‘𝐵)‘𝑛)))
91	4, 89, 90	sylanbrc 594	1 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (reverse‘𝐵) ∈ (^◡ < Chain 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 400 = wceq 1568 ∈ wcel 2141 ≠ wne 2956 ∉ wnel 3062 ∀wral 3077 ∖ cdif 3901 ⊆ wss 3904 {csn 4588 class class class wbr 5108 ^◡ccnv 5660 dom cdm 5661 ‘cfv 6536 (class class class)co 7410 ℂcc 11097 0cc0 11099 1c1 11100 + caddc 11102 ≤ cle 11243 − cmin 11440 ℕcn 12232 ℕ₀cn0 12503 ℤcz 12590 ...cfz 13534 ..^cfzo 13681 ♯chash 14365 Word cword 14549 reversecreverse 14794 Chain cchn 18660

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1823 ax-4 1837 ax-5 1938 ax-6 1995 ax-7 2036 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1571 df-fal 1581 df-ex 1808 df-nf 1812 df-sb 2095 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-er 8693 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-n0 12504 df-z 12591 df-uz 12862 df-fz 13535 df-fzo 13682 df-hash 14366 df-word 14550 df-reverse 14795 df-chn 18661

This theorem is referenced by: (None)

W3C validator