znleval - Metamath Proof Explorer

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

Theorem znleval 21110

Description: The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.)

**Hypotheses**
Ref	Expression
znle2.y	⊢ 𝑌 = (ℤ/nℤ‘𝑁)
znle2.f	⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)
znle2.w	⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))
znle2.l	⊢ ≤ = (le‘𝑌)
znleval.x	⊢ 𝑋 = (Base‘𝑌)

**Assertion**
Ref	Expression
znleval	⊢ (𝑁 ∈ ℕ₀ → (𝐴 ≤ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵))))

Proof of Theorem znleval Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		znle2.y	. . . . . . 7 ⊢ 𝑌 = (ℤ/nℤ‘𝑁)
2		znle2.f	. . . . . . 7 ⊢ 𝐹 = ((ℤRHom‘𝑌) ↾ 𝑊)
3		znle2.w	. . . . . . 7 ⊢ 𝑊 = if(𝑁 = 0, ℤ, (0..^𝑁))
4		znle2.l	. . . . . . 7 ⊢ ≤ = (le‘𝑌)
5	1, 2, 3, 4	znle2 21109	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ≤ = ((𝐹 ∘ ≤ ) ∘ ^◡𝐹))
6		relco 6108	. . . . . . . 8 ⊢ Rel ((𝐹 ∘ ≤ ) ∘ ^◡𝐹)
7		relssdmrn 6268	. . . . . . . 8 ⊢ (Rel ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) → ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹)))
8	6, 7	ax-mp 5	. . . . . . 7 ⊢ ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹))
9		dmcoss 5971	. . . . . . . . 9 ⊢ dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ dom ^◡𝐹
10		df-rn 5688	. . . . . . . . . 10 ⊢ ran 𝐹 = dom ^◡𝐹
11		znleval.x	. . . . . . . . . . . 12 ⊢ 𝑋 = (Base‘𝑌)
12	1, 11, 2, 3	znf1o 21107	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → 𝐹:𝑊–1-1-onto→𝑋)
13		f1ofo 6841	. . . . . . . . . . 11 ⊢ (𝐹:𝑊–1-1-onto→𝑋 → 𝐹:𝑊–onto→𝑋)
14		forn 6809	. . . . . . . . . . 11 ⊢ (𝐹:𝑊–onto→𝑋 → ran 𝐹 = 𝑋)
15	12, 13, 14	3syl 18	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → ran 𝐹 = 𝑋)
16	10, 15	eqtr3id 2787	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → dom ^◡𝐹 = 𝑋)
17	9, 16	sseqtrid 4035	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ 𝑋)
18		rncoss 5972	. . . . . . . . 9 ⊢ ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ ran (𝐹 ∘ ≤ )
19		rncoss 5972	. . . . . . . . . 10 ⊢ ran (𝐹 ∘ ≤ ) ⊆ ran 𝐹
20	19, 15	sseqtrid 4035	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → ran (𝐹 ∘ ≤ ) ⊆ 𝑋)
21	18, 20	sstrid 3994	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ 𝑋)
22		xpss12 5692	. . . . . . . 8 ⊢ ((dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ 𝑋 ∧ ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ 𝑋) → (dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹)) ⊆ (𝑋 × 𝑋))
23	17, 21, 22	syl2anc 585	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹)) ⊆ (𝑋 × 𝑋))
24	8, 23	sstrid 3994	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ (𝑋 × 𝑋))
25	5, 24	eqsstrd 4021	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → ≤ ⊆ (𝑋 × 𝑋))
26	25	ssbrd 5192	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ≤ 𝐵 → 𝐴(𝑋 × 𝑋)𝐵))
27		brxp 5726	. . . 4 ⊢ (𝐴(𝑋 × 𝑋)𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋))
28	26, 27	imbitrdi 250	. . 3 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ≤ 𝐵 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)))
29	28	pm4.71rd 564	. 2 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ≤ 𝐵 ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵)))
30	5	adantr 482	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ≤ = ((𝐹 ∘ ≤ ) ∘ ^◡𝐹))
31	30	breqd 5160	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴 ≤ 𝐵 ↔ 𝐴((𝐹 ∘ ≤ ) ∘ ^◡𝐹)𝐵))
32		brcog 5867	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴((𝐹 ∘ ≤ ) ∘ ^◡𝐹)𝐵 ↔ ∃𝑥(𝐴^◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
33	32	adantl 483	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ ^◡𝐹)𝐵 ↔ ∃𝑥(𝐴^◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
34		eqcom 2740	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝐹‘𝐴) ↔ (^◡𝐹‘𝐴) = 𝑥)
35	12	adantr 482	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐹:𝑊–1-1-onto→𝑋)
36		f1ocnv 6846	. . . . . . . . . . 11 ⊢ (𝐹:𝑊–1-1-onto→𝑋 → ^◡𝐹:𝑋–1-1-onto→𝑊)
37		f1ofn 6835	. . . . . . . . . . 11 ⊢ (^◡𝐹:𝑋–1-1-onto→𝑊 → ^◡𝐹 Fn 𝑋)
38	35, 36, 37	3syl 18	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ^◡𝐹 Fn 𝑋)
39		simprl 770	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐴 ∈ 𝑋)
40		fnbrfvb 6945	. . . . . . . . . 10 ⊢ ((^◡𝐹 Fn 𝑋 ∧ 𝐴 ∈ 𝑋) → ((^◡𝐹‘𝐴) = 𝑥 ↔ 𝐴^◡𝐹𝑥))
41	38, 39, 40	syl2anc 585	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((^◡𝐹‘𝐴) = 𝑥 ↔ 𝐴^◡𝐹𝑥))
42	34, 41	bitr2id 284	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴^◡𝐹𝑥 ↔ 𝑥 = (^◡𝐹‘𝐴)))
43	42	anbi1d 631	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝐴^◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (𝑥 = (^◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
44	43	exbidv 1925	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝐴^◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ ∃𝑥(𝑥 = (^◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
45	33, 44	bitrd 279	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ ^◡𝐹)𝐵 ↔ ∃𝑥(𝑥 = (^◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
46		fvex 6905	. . . . . . 7 ⊢ (^◡𝐹‘𝐴) ∈ V
47		breq1 5152	. . . . . . 7 ⊢ (𝑥 = (^◡𝐹‘𝐴) → (𝑥(𝐹 ∘ ≤ )𝐵 ↔ (^◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵))
48	46, 47	ceqsexv 3526	. . . . . 6 ⊢ (∃𝑥(𝑥 = (^◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (^◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵)
49		simprr 772	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐵 ∈ 𝑋)
50		brcog 5867	. . . . . . . 8 ⊢ (((^◡𝐹‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑋) → ((^◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((^◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵)))
51	46, 49, 50	sylancr 588	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((^◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((^◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵)))
52		fvex 6905	. . . . . . . . 9 ⊢ (^◡𝐹‘𝐵) ∈ V
53		breq2 5153	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝐹‘𝐵) → ((^◡𝐹‘𝐴) ≤ 𝑥 ↔ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵)))
54	52, 53	ceqsexv 3526	. . . . . . . 8 ⊢ (∃𝑥(𝑥 = (^◡𝐹‘𝐵) ∧ (^◡𝐹‘𝐴) ≤ 𝑥) ↔ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵))
55		eqcom 2740	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹‘𝐵) ↔ (^◡𝐹‘𝐵) = 𝑥)
56		fnbrfvb 6945	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹 Fn 𝑋 ∧ 𝐵 ∈ 𝑋) → ((^◡𝐹‘𝐵) = 𝑥 ↔ 𝐵^◡𝐹𝑥))
57	38, 49, 56	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((^◡𝐹‘𝐵) = 𝑥 ↔ 𝐵^◡𝐹𝑥))
58	55, 57	bitrid 283	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑥 = (^◡𝐹‘𝐵) ↔ 𝐵^◡𝐹𝑥))
59		vex 3479	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
60		brcnvg 5880	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ 𝑋 ∧ 𝑥 ∈ V) → (𝐵^◡𝐹𝑥 ↔ 𝑥𝐹𝐵))
61	49, 59, 60	sylancl 587	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐵^◡𝐹𝑥 ↔ 𝑥𝐹𝐵))
62	58, 61	bitrd 279	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑥 = (^◡𝐹‘𝐵) ↔ 𝑥𝐹𝐵))
63	62	anbi1d 631	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝑥 = (^◡𝐹‘𝐵) ∧ (^◡𝐹‘𝐴) ≤ 𝑥) ↔ (𝑥𝐹𝐵 ∧ (^◡𝐹‘𝐴) ≤ 𝑥)))
64	63	biancomd 465	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((𝑥 = (^◡𝐹‘𝐵) ∧ (^◡𝐹‘𝐴) ≤ 𝑥) ↔ ((^◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵)))
65	64	exbidv 1925	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝑥 = (^◡𝐹‘𝐵) ∧ (^◡𝐹‘𝐴) ≤ 𝑥) ↔ ∃𝑥((^◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵)))
66	54, 65	bitr3id 285	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵) ↔ ∃𝑥((^◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵)))
67	51, 66	bitr4d 282	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((^◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵)))
68	48, 67	bitrid 283	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (∃𝑥(𝑥 = (^◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵)))
69	31, 45, 68	3bitrd 305	. . . 4 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴 ≤ 𝐵 ↔ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵)))
70	69	pm5.32da 580	. . 3 ⊢ (𝑁 ∈ ℕ₀ → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵))))
71		df-3an 1090	. . 3 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵)) ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵)))
72	70, 71	bitr4di 289	. 2 ⊢ (𝑁 ∈ ℕ₀ → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵) ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵))))
73	29, 72	bitrd 279	1 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ≤ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∃wex 1782 ∈ wcel 2107 Vcvv 3475 ⊆ wss 3949 ifcif 4529 class class class wbr 5149 × cxp 5675 ^◡ccnv 5676 dom cdm 5677 ran crn 5678 ↾ cres 5679 ∘ ccom 5681 Rel wrel 5682 Fn wfn 6539 –onto→wfo 6542 –1-1-onto→wf1o 6543 ‘cfv 6544 (class class class)co 7409 0cc0 11110 ≤ cle 11249 ℕ₀cn0 12472 ℤcz 12558 ..^cfzo 13627 Basecbs 17144 lecple 17204 ℤRHomczrh 21049 ℤ/nℤczn 21052

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-pre-sup 11188 ax-addf 11189 ax-mulf 11190

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-tpos 8211 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-er 8703 df-ec 8705 df-qs 8709 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9437 df-inf 9438 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-7 12280 df-8 12281 df-9 12282 df-n0 12473 df-z 12559 df-dec 12678 df-uz 12823 df-rp 12975 df-fz 13485 df-fzo 13628 df-fl 13757 df-mod 13835 df-seq 13967 df-dvds 16198 df-struct 17080 df-sets 17097 df-slot 17115 df-ndx 17127 df-base 17145 df-ress 17174 df-plusg 17210 df-mulr 17211 df-starv 17212 df-sca 17213 df-vsca 17214 df-ip 17215 df-tset 17216 df-ple 17217 df-ds 17219 df-unif 17220 df-0g 17387 df-imas 17454 df-qus 17455 df-mgm 18561 df-sgrp 18610 df-mnd 18626 df-mhm 18671 df-grp 18822 df-minusg 18823 df-sbg 18824 df-mulg 18951 df-subg 19003 df-nsg 19004 df-eqg 19005 df-ghm 19090 df-cmn 19650 df-abl 19651 df-mgp 19988 df-ur 20005 df-ring 20058 df-cring 20059 df-oppr 20150 df-dvdsr 20171 df-rnghom 20251 df-subrg 20317 df-lmod 20473 df-lss 20543 df-lsp 20583 df-sra 20785 df-rgmod 20786 df-lidl 20787 df-rsp 20788 df-2idl 20857 df-cnfld 20945 df-zring 21018 df-zrh 21053 df-zn 21056

This theorem is referenced by: znleval2 21111

W3C validator