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 18582

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 22	. . . 4 ⊢ (𝐵 ∈ ( < Chain 𝐴) → 𝐵 ∈ ( < Chain 𝐴))
2	1	chnwrd 18563	. . 3 ⊢ (𝐵 ∈ ( < Chain 𝐴) → 𝐵 ∈ Word 𝐴)
3		revcl 14712	. . 3 ⊢ (𝐵 ∈ Word 𝐴 → (reverse‘𝐵) ∈ Word 𝐴)
4	2, 3	syl 17	. 2 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (reverse‘𝐵) ∈ Word 𝐴)
5		simpl 482	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝐵 ∈ ( < Chain 𝐴))
6		fzossfz 13622	. . . . . . . . . . . . . . 15 ⊢ (0..^(♯‘(reverse‘𝐵))) ⊆ (0...(♯‘(reverse‘𝐵)))
7	6	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (0..^(♯‘(reverse‘𝐵))) ⊆ (0...(♯‘(reverse‘𝐵))))
8		wrddm 14472	. . . . . . . . . . . . . . 15 ⊢ ((reverse‘𝐵) ∈ Word 𝐴 → dom (reverse‘𝐵) = (0..^(♯‘(reverse‘𝐵))))
9	4, 8	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ( < Chain 𝐴) → dom (reverse‘𝐵) = (0..^(♯‘(reverse‘𝐵))))
10		revlen 14713	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵 ∈ Word 𝐴 → (♯‘(reverse‘𝐵)) = (♯‘𝐵))
11	2, 10	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (♯‘(reverse‘𝐵)) = (♯‘𝐵))
12	11	eqcomd 2741	. . . . . . . . . . . . . . 15 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (♯‘𝐵) = (♯‘(reverse‘𝐵)))
13	12	oveq2d 7372	. . . . . . . . . . . . . 14 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (0...(♯‘𝐵)) = (0...(♯‘(reverse‘𝐵))))
14	7, 9, 13	3sstr4d 3972	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ( < Chain 𝐴) → dom (reverse‘𝐵) ⊆ (0...(♯‘𝐵)))
15	14	ssdifd 4077	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (dom (reverse‘𝐵) ∖ {0}) ⊆ ((0...(♯‘𝐵)) ∖ {0}))
16	15	sselda 3917	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ ((0...(♯‘𝐵)) ∖ {0}))
17	2	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝐵 ∈ Word 𝐴)
18		lencl 14484	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ Word 𝐴 → (♯‘𝐵) ∈ ℕ₀)
19	17, 18	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) ∈ ℕ₀)
20		fz0dif1 13549	. . . . . . . . . . . 12 ⊢ ((♯‘𝐵) ∈ ℕ₀ → ((0...(♯‘𝐵)) ∖ {0}) = (1...(♯‘𝐵)))
21	19, 20	syl 17	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((0...(♯‘𝐵)) ∖ {0}) = (1...(♯‘𝐵)))
22	16, 21	eleqtrd 2837	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ (1...(♯‘𝐵)))
23		ubmelfzo 13674	. . . . . . . . . 10 ⊢ (𝑛 ∈ (1...(♯‘𝐵)) → ((♯‘𝐵) − 𝑛) ∈ (0..^(♯‘𝐵)))
24	22, 23	syl 17	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘𝐵) − 𝑛) ∈ (0..^(♯‘𝐵)))
25		wrddm 14472	. . . . . . . . . 10 ⊢ (𝐵 ∈ Word 𝐴 → dom 𝐵 = (0..^(♯‘𝐵)))
26	17, 25	syl 17	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → dom 𝐵 = (0..^(♯‘𝐵)))
27	24, 26	eleqtrrd 2838	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘𝐵) − 𝑛) ∈ dom 𝐵)
28	19	nn0cnd 12489	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) ∈ ℂ)
29		eldifi 4063	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (dom (reverse‘𝐵) ∖ {0}) → 𝑛 ∈ dom (reverse‘𝐵))
30	29	anim2i 618	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ dom (reverse‘𝐵)))
31	2, 3, 8	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ( < Chain 𝐴) → dom (reverse‘𝐵) = (0..^(♯‘(reverse‘𝐵))))
32	31	eleq2d 2821	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (𝑛 ∈ dom (reverse‘𝐵) ↔ 𝑛 ∈ (0..^(♯‘(reverse‘𝐵)))))
33	32	biimpa 476	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ dom (reverse‘𝐵)) → 𝑛 ∈ (0..^(♯‘(reverse‘𝐵))))
34		elfzoelz 13602	. . . . . . . . . . 11 ⊢ (𝑛 ∈ (0..^(♯‘(reverse‘𝐵))) → 𝑛 ∈ ℤ)
35	33, 34	syl 17	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ dom (reverse‘𝐵)) → 𝑛 ∈ ℤ)
36		zcn 12518	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
37	30, 35, 36	3syl 18	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ ℂ)
38	29	adantl 481	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ dom (reverse‘𝐵))
39	17, 3	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (reverse‘𝐵) ∈ Word 𝐴)
40		wrdlndm 14481	. . . . . . . . . . . . 13 ⊢ ((reverse‘𝐵) ∈ Word 𝐴 → (♯‘(reverse‘𝐵)) ∉ dom (reverse‘𝐵))
41	39, 40	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘(reverse‘𝐵)) ∉ dom (reverse‘𝐵))
42	17, 10	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘(reverse‘𝐵)) = (♯‘𝐵))
43		eqidd 2736	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → dom (reverse‘𝐵) = dom (reverse‘𝐵))
44	42, 43	neleq12d 3039	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘(reverse‘𝐵)) ∉ dom (reverse‘𝐵) ↔ (♯‘𝐵) ∉ dom (reverse‘𝐵)))
45	41, 44	mpbid 232	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) ∉ dom (reverse‘𝐵))
46		elnelne2 3046	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ dom (reverse‘𝐵) ∧ (♯‘𝐵) ∉ dom (reverse‘𝐵)) → 𝑛 ≠ (♯‘𝐵))
47	38, 45, 46	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ≠ (♯‘𝐵))
48	47	necomd 2985	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) ≠ 𝑛)
49	28, 37, 48	subne0d 11503	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘𝐵) − 𝑛) ≠ 0)
50	27, 49	eldifsnd 4722	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((♯‘𝐵) − 𝑛) ∈ (dom 𝐵 ∖ {0}))
51	5, 50	chnltm1 18564	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 𝑛) − 1)) < (𝐵‘((♯‘𝐵) − 𝑛)))
52		1cnd 11128	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 1 ∈ ℂ)
53	28, 52, 37	sub32d 11526	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (((♯‘𝐵) − 1) − 𝑛) = (((♯‘𝐵) − 𝑛) − 1))
54	53	fveq2d 6833	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) = (𝐵‘(((♯‘𝐵) − 𝑛) − 1)))
55	28, 37, 52	nnncan2d 11529	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (((♯‘𝐵) − 1) − (𝑛 − 1)) = ((♯‘𝐵) − 𝑛))
56	55	fveq2d 6833	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))) = (𝐵‘((♯‘𝐵) − 𝑛)))
57	51, 54, 56	3brtr4d 5106	. . . . 5 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) < (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))))
58		fvex 6842	. . . . . 6 ⊢ (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))) ∈ V
59		fvex 6842	. . . . . 6 ⊢ (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) ∈ V
60	58, 59	brcnv 5826	. . . . 5 ⊢ ((𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1)))^◡ < (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) ↔ (𝐵‘(((♯‘𝐵) − 1) − 𝑛)) < (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))))
61	57, 60	sylibr 234	. . . 4 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1)))^◡ < (𝐵‘(((♯‘𝐵) − 1) − 𝑛)))
62	39, 8	syl 17	. . . . . . . . . 10 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → dom (reverse‘𝐵) = (0..^(♯‘(reverse‘𝐵))))
63	38, 62	eleqtrd 2837	. . . . . . . . 9 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ (0..^(♯‘(reverse‘𝐵))))
64		elfzonn0 13651	. . . . . . . . 9 ⊢ (𝑛 ∈ (0..^(♯‘(reverse‘𝐵))) → 𝑛 ∈ ℕ₀)
65	63, 64	syl 17	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ ℕ₀)
66		eldifsni 4725	. . . . . . . . 9 ⊢ (𝑛 ∈ (dom (reverse‘𝐵) ∖ {0}) → 𝑛 ≠ 0)
67	66	adantl 481	. . . . . . . 8 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ≠ 0)
68		elnnne0 12440	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℕ₀ ∧ 𝑛 ≠ 0))
69	65, 67, 68	sylanbrc 584	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ ℕ)
70		nnm1nn0 12467	. . . . . . 7 ⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈ ℕ₀)
71	69, 70	syl 17	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝑛 − 1) ∈ ℕ₀)
72		elfzo0le 13647	. . . . . . . 8 ⊢ (𝑛 ∈ (0..^(♯‘(reverse‘𝐵))) → 𝑛 ≤ (♯‘(reverse‘𝐵)))
73	63, 72	syl 17	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ≤ (♯‘(reverse‘𝐵)))
74	37, 52	npcand 11498	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((𝑛 − 1) + 1) = 𝑛)
75	42	eqcomd 2741	. . . . . . 7 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (♯‘𝐵) = (♯‘(reverse‘𝐵)))
76	73, 74, 75	3brtr4d 5106	. . . . . 6 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((𝑛 − 1) + 1) ≤ (♯‘𝐵))
77		nn0p1elfzo 13646	. . . . . 6 ⊢ (((𝑛 − 1) ∈ ℕ₀ ∧ (♯‘𝐵) ∈ ℕ₀ ∧ ((𝑛 − 1) + 1) ≤ (♯‘𝐵)) → (𝑛 − 1) ∈ (0..^(♯‘𝐵)))
78	71, 19, 76, 77	syl3anc 1374	. . . . 5 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → (𝑛 − 1) ∈ (0..^(♯‘𝐵)))
79		revfv 14714	. . . . 5 ⊢ ((𝐵 ∈ Word 𝐴 ∧ (𝑛 − 1) ∈ (0..^(♯‘𝐵))) → ((reverse‘𝐵)‘(𝑛 − 1)) = (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))))
80	17, 78, 79	syl2anc 585	. . . 4 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((reverse‘𝐵)‘(𝑛 − 1)) = (𝐵‘(((♯‘𝐵) − 1) − (𝑛 − 1))))
81	11	oveq2d 7372	. . . . . . . . 9 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (0..^(♯‘(reverse‘𝐵))) = (0..^(♯‘𝐵)))
82	31, 81	eqtrd 2770	. . . . . . . 8 ⊢ (𝐵 ∈ ( < Chain 𝐴) → dom (reverse‘𝐵) = (0..^(♯‘𝐵)))
83	82	eleq2d 2821	. . . . . . 7 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (𝑛 ∈ dom (reverse‘𝐵) ↔ 𝑛 ∈ (0..^(♯‘𝐵))))
84	29, 83	imbitrid 244	. . . . . 6 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (𝑛 ∈ (dom (reverse‘𝐵) ∖ {0}) → 𝑛 ∈ (0..^(♯‘𝐵))))
85	84	imp 406	. . . . 5 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → 𝑛 ∈ (0..^(♯‘𝐵)))
86		revfv 14714	. . . . 5 ⊢ ((𝐵 ∈ Word 𝐴 ∧ 𝑛 ∈ (0..^(♯‘𝐵))) → ((reverse‘𝐵)‘𝑛) = (𝐵‘(((♯‘𝐵) − 1) − 𝑛)))
87	17, 85, 86	syl2anc 585	. . . 4 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((reverse‘𝐵)‘𝑛) = (𝐵‘(((♯‘𝐵) − 1) − 𝑛)))
88	61, 80, 87	3brtr4d 5106	. . 3 ⊢ ((𝐵 ∈ ( < Chain 𝐴) ∧ 𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})) → ((reverse‘𝐵)‘(𝑛 − 1))^◡ < ((reverse‘𝐵)‘𝑛))
89	88	ralrimiva 3127	. 2 ⊢ (𝐵 ∈ ( < Chain 𝐴) → ∀𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})((reverse‘𝐵)‘(𝑛 − 1))^◡ < ((reverse‘𝐵)‘𝑛))
90		ischn 18562	. 2 ⊢ ((reverse‘𝐵) ∈ (^◡ < Chain 𝐴) ↔ ((reverse‘𝐵) ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom (reverse‘𝐵) ∖ {0})((reverse‘𝐵)‘(𝑛 − 1))^◡ < ((reverse‘𝐵)‘𝑛)))
91	4, 89, 90	sylanbrc 584	1 ⊢ (𝐵 ∈ ( < Chain 𝐴) → (reverse‘𝐵) ∈ (^◡ < Chain 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2930 ∉ wnel 3034 ∀wral 3049 ∖ cdif 3882 ⊆ wss 3885 {csn 4557 class class class wbr 5074 ^◡ccnv 5619 dom cdm 5620 ‘cfv 6487 (class class class)co 7356 ℂcc 11025 0cc0 11027 1c1 11028 + caddc 11030 ≤ cle 11169 − cmin 11366 ℕcn 12163 ℕ₀cn0 12426 ℤcz 12513 ...cfz 13450 ..^cfzo 13597 ♯chash 14281 Word cword 14464 reversecreverse 14709 Chain cchn 18560

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2184 ax-ext 2707 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7678 ax-cnex 11083 ax-resscn 11084 ax-1cn 11085 ax-icn 11086 ax-addcl 11087 ax-addrcl 11088 ax-mulcl 11089 ax-mulrcl 11090 ax-mulcom 11091 ax-addass 11092 ax-mulass 11093 ax-distr 11094 ax-i2m1 11095 ax-1ne0 11096 ax-1rid 11097 ax-rnegex 11098 ax-rrecex 11099 ax-cnre 11100 ax-pre-lttri 11101 ax-pre-lttrn 11102 ax-pre-ltadd 11103 ax-pre-mulgt0 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2538 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2810 df-nfc 2884 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3060 df-reu 3341 df-rab 3388 df-v 3429 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4264 df-if 4457 df-pw 4533 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4841 df-int 4880 df-iun 4925 df-br 5075 df-opab 5137 df-mpt 5156 df-tr 5182 df-id 5515 df-eprel 5520 df-po 5528 df-so 5529 df-fr 5573 df-we 5575 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6254 df-ord 6315 df-on 6316 df-lim 6317 df-suc 6318 df-iota 6443 df-fun 6489 df-fn 6490 df-f 6491 df-f1 6492 df-fo 6493 df-f1o 6494 df-fv 6495 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-er 8632 df-en 8883 df-dom 8884 df-sdom 8885 df-fin 8886 df-card 9852 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-nn 12164 df-n0 12427 df-z 12514 df-uz 12778 df-fz 13451 df-fzo 13598 df-hash 14282 df-word 14465 df-reverse 14710 df-chn 18561

This theorem is referenced by: (None)

W3C validator