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 21102

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 21101	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ≤ = ((𝐹 ∘ ≤ ) ∘ ^◡𝐹))
6		relco 6105	. . . . . . . 8 ⊢ Rel ((𝐹 ∘ ≤ ) ∘ ^◡𝐹)
7		relssdmrn 6265	. . . . . . . 8 ⊢ (Rel ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) → ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹)))
8	6, 7	ax-mp 5	. . . . . . 7 ⊢ ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ (dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹))
9		dmcoss 5969	. . . . . . . . 9 ⊢ dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ dom ^◡𝐹
10		df-rn 5687	. . . . . . . . . 10 ⊢ ran 𝐹 = dom ^◡𝐹
11		znleval.x	. . . . . . . . . . . 12 ⊢ 𝑋 = (Base‘𝑌)
12	1, 11, 2, 3	znf1o 21099	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → 𝐹:𝑊–1-1-onto→𝑋)
13		f1ofo 6838	. . . . . . . . . . 11 ⊢ (𝐹:𝑊–1-1-onto→𝑋 → 𝐹:𝑊–onto→𝑋)
14		forn 6806	. . . . . . . . . . 11 ⊢ (𝐹:𝑊–onto→𝑋 → ran 𝐹 = 𝑋)
15	12, 13, 14	3syl 18	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → ran 𝐹 = 𝑋)
16	10, 15	eqtr3id 2787	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → dom ^◡𝐹 = 𝑋)
17	9, 16	sseqtrid 4034	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ 𝑋)
18		rncoss 5970	. . . . . . . . 9 ⊢ ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ ran (𝐹 ∘ ≤ )
19		rncoss 5970	. . . . . . . . . 10 ⊢ ran (𝐹 ∘ ≤ ) ⊆ ran 𝐹
20	19, 15	sseqtrid 4034	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → ran (𝐹 ∘ ≤ ) ⊆ 𝑋)
21	18, 20	sstrid 3993	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ 𝑋)
22		xpss12 5691	. . . . . . . 8 ⊢ ((dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ 𝑋 ∧ ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ 𝑋) → (dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹)) ⊆ (𝑋 × 𝑋))
23	17, 21, 22	syl2anc 585	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (dom ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) × ran ((𝐹 ∘ ≤ ) ∘ ^◡𝐹)) ⊆ (𝑋 × 𝑋))
24	8, 23	sstrid 3993	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → ((𝐹 ∘ ≤ ) ∘ ^◡𝐹) ⊆ (𝑋 × 𝑋))
25	5, 24	eqsstrd 4020	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → ≤ ⊆ (𝑋 × 𝑋))
26	25	ssbrd 5191	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ≤ 𝐵 → 𝐴(𝑋 × 𝑋)𝐵))
27		brxp 5724	. . . 4 ⊢ (𝐴(𝑋 × 𝑋)𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋))
28	26, 27	imbitrdi 250	. . 3 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ≤ 𝐵 → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)))
29	28	pm4.71rd 564	. 2 ⊢ (𝑁 ∈ ℕ₀ → (𝐴 ≤ 𝐵 ↔ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ 𝐴 ≤ 𝐵)))
30	5	adantr 482	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ≤ = ((𝐹 ∘ ≤ ) ∘ ^◡𝐹))
31	30	breqd 5159	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴 ≤ 𝐵 ↔ 𝐴((𝐹 ∘ ≤ ) ∘ ^◡𝐹)𝐵))
32		brcog 5865	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴((𝐹 ∘ ≤ ) ∘ ^◡𝐹)𝐵 ↔ ∃𝑥(𝐴^◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
33	32	adantl 483	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴((𝐹 ∘ ≤ ) ∘ ^◡𝐹)𝐵 ↔ ∃𝑥(𝐴^◡𝐹𝑥 ∧ 𝑥(𝐹 ∘ ≤ )𝐵)))
34		eqcom 2740	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝐹‘𝐴) ↔ (^◡𝐹‘𝐴) = 𝑥)
35	12	adantr 482	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐹:𝑊–1-1-onto→𝑋)
36		f1ocnv 6843	. . . . . . . . . . 11 ⊢ (𝐹:𝑊–1-1-onto→𝑋 → ^◡𝐹:𝑋–1-1-onto→𝑊)
37		f1ofn 6832	. . . . . . . . . . 11 ⊢ (^◡𝐹:𝑋–1-1-onto→𝑊 → ^◡𝐹 Fn 𝑋)
38	35, 36, 37	3syl 18	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ^◡𝐹 Fn 𝑋)
39		simprl 770	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐴 ∈ 𝑋)
40		fnbrfvb 6942	. . . . . . . . . 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 6902	. . . . . . 7 ⊢ (^◡𝐹‘𝐴) ∈ V
47		breq1 5151	. . . . . . 7 ⊢ (𝑥 = (^◡𝐹‘𝐴) → (𝑥(𝐹 ∘ ≤ )𝐵 ↔ (^◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵))
48	46, 47	ceqsexv 3526	. . . . . 6 ⊢ (∃𝑥(𝑥 = (^◡𝐹‘𝐴) ∧ 𝑥(𝐹 ∘ ≤ )𝐵) ↔ (^◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵)
49		simprr 772	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝐵 ∈ 𝑋)
50		brcog 5865	. . . . . . . 8 ⊢ (((^◡𝐹‘𝐴) ∈ V ∧ 𝐵 ∈ 𝑋) → ((^◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((^◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵)))
51	46, 49, 50	sylancr 588	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((^◡𝐹‘𝐴)(𝐹 ∘ ≤ )𝐵 ↔ ∃𝑥((^◡𝐹‘𝐴) ≤ 𝑥 ∧ 𝑥𝐹𝐵)))
52		fvex 6902	. . . . . . . . 9 ⊢ (^◡𝐹‘𝐵) ∈ V
53		breq2 5152	. . . . . . . . 9 ⊢ (𝑥 = (^◡𝐹‘𝐵) → ((^◡𝐹‘𝐴) ≤ 𝑥 ↔ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵)))
54	52, 53	ceqsexv 3526	. . . . . . . 8 ⊢ (∃𝑥(𝑥 = (^◡𝐹‘𝐵) ∧ (^◡𝐹‘𝐴) ≤ 𝑥) ↔ (^◡𝐹‘𝐴) ≤ (^◡𝐹‘𝐵))
55		eqcom 2740	. . . . . . . . . . . . 13 ⊢ (𝑥 = (^◡𝐹‘𝐵) ↔ (^◡𝐹‘𝐵) = 𝑥)
56		fnbrfvb 6942	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹 Fn 𝑋 ∧ 𝐵 ∈ 𝑋) → ((^◡𝐹‘𝐵) = 𝑥 ↔ 𝐵^◡𝐹𝑥))
57	38, 49, 56	syl2anc 585	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((^◡𝐹‘𝐵) = 𝑥 ↔ 𝐵^◡𝐹𝑥))
58	55, 57	bitrid 283	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑥 = (^◡𝐹‘𝐵) ↔ 𝐵^◡𝐹𝑥))
59		vex 3479	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
60		brcnvg 5878	. . . . . . . . . . . . 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 3948 ifcif 4528 class class class wbr 5148 × cxp 5674 ^◡ccnv 5675 dom cdm 5676 ran crn 5677 ↾ cres 5678 ∘ ccom 5680 Rel wrel 5681 Fn wfn 6536 –onto→wfo 6539 –1-1-onto→wf1o 6540 ‘cfv 6541 (class class class)co 7406 0cc0 11107 ≤ cle 11246 ℕ₀cn0 12469 ℤcz 12555 ..^cfzo 13624 Basecbs 17141 lecple 17201 ℤRHomczrh 21041 ℤ/nℤczn 21044

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 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

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 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-om 7853 df-1st 7972 df-2nd 7973 df-tpos 8208 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-er 8700 df-ec 8702 df-qs 8706 df-map 8819 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-sup 9434 df-inf 9435 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-rp 12972 df-fz 13482 df-fzo 13625 df-fl 13754 df-mod 13832 df-seq 13964 df-dvds 16195 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-0g 17384 df-imas 17451 df-qus 17452 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-mhm 18668 df-grp 18819 df-minusg 18820 df-sbg 18821 df-mulg 18946 df-subg 18998 df-nsg 18999 df-eqg 19000 df-ghm 19085 df-cmn 19645 df-abl 19646 df-mgp 19983 df-ur 20000 df-ring 20052 df-cring 20053 df-oppr 20143 df-dvdsr 20164 df-rnghom 20244 df-subrg 20354 df-lmod 20466 df-lss 20536 df-lsp 20576 df-sra 20778 df-rgmod 20779 df-lidl 20780 df-rsp 20781 df-2idl 20850 df-cnfld 20938 df-zring 21011 df-zrh 21045 df-zn 21048

This theorem is referenced by: znleval2 21103

W3C validator