ispridlc - Mathbox for Jeff Madsen

	Mathbox for Jeff Madsen		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ispridlc		Structured version Visualization version GIF version

Theorem ispridlc 38054

Description: The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.)

**Hypotheses**
Ref	Expression
ispridlc.1	⊢ 𝐺 = (1^st ‘𝑅)
ispridlc.2	⊢ 𝐻 = (2^nd ‘𝑅)
ispridlc.3	⊢ 𝑋 = ran 𝐺

**Assertion**
Ref	Expression
ispridlc	⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))

Distinct variable groups: 𝑅,𝑎,𝑏 𝑃,𝑎,𝑏 𝑋,𝑎,𝑏 𝐻,𝑎,𝑏 Allowed substitution hints: 𝐺(𝑎,𝑏)

Proof of Theorem ispridlc Dummy variables 𝑥 𝑦 𝑟 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		crngorngo 37984	. . . 4 ⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps)
2		ispridlc.1	. . . . 5 ⊢ 𝐺 = (1^st ‘𝑅)
3		ispridlc.2	. . . . 5 ⊢ 𝐻 = (2^nd ‘𝑅)
4		ispridlc.3	. . . . 5 ⊢ 𝑋 = ran 𝐺
5	2, 3, 4	ispridl 38018	. . . 4 ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
6	1, 5	syl 17	. . 3 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
7		snssi 4759	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑋 → {𝑎} ⊆ 𝑋)
8	2, 4	igenidl 38047	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
9	1, 7, 8	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
10	9	adantrr 717	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
11		snssi 4759	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝑋 → {𝑏} ⊆ 𝑋)
12	2, 4	igenidl 38047	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
13	1, 11, 12	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
14	13	adantrl 716	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
15		raleq 3286	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃))
16		sseq1 3961	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (𝑟 ⊆ 𝑃 ↔ (𝑅 IdlGen {𝑎}) ⊆ 𝑃))
17	16	orbi1d 916	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))
18	15, 17	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))))
19		raleq 3286	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
20	19	ralbidv 3152	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
21		sseq1 3961	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (𝑠 ⊆ 𝑃 ↔ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))
22	21	orbi2d 915	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)))
23	20, 22	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
24	18, 23	rspc2v 3588	. . . . . . . . . . 11 ⊢ (((𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅) ∧ (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
25	10, 14, 24	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
26	25	adantlr 715	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
27	2, 3, 4	prnc 38051	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)})
28		df-rab 3395	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)} = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))}
29	27, 28	eqtrdi 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))})
30	29	eqabrd 2870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
31	30	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
32	2, 3, 4	prnc 38051	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)})
33		df-rab 3395	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)} = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))}
34	32, 33	eqtrdi 2780	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))})
35	34	eqabrd 2870	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
36	35	adantrl 716	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
37	31, 36	anbi12d 632	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))))
38	37	adantlr 715	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))))
39	38	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))))
40		reeanv 3201	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) ↔ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))
41	40	anbi2i 623	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
42		an4 656	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
43	41, 42	bitri 275	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
44	2, 3, 4	crngm4 37987	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
45	44	3com23 1126	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
46	45	3expa 1118	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
47	46	adantllr 719	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
48	47	adantlr 715	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
49	2, 3, 4	rngocl 37885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
50	1, 49	syl3an1 1163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
51	50	3expb 1120	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
52	51	adantlr 715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
53	52	adantlr 715	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
54	2, 3, 4	idllmulcl 38004	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
55	1, 54	sylanl1 680	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
56	55	anassrs 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝐻𝑠) ∈ 𝑋) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
57	53, 56	syldan 591	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
58	57	adantllr 719	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
59	48, 58	eqeltrrd 2829	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃)
60		oveq12 7358	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
61	60	eleq1d 2813	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → ((𝑥𝐻𝑦) ∈ 𝑃 ↔ ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃))
62	59, 61	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
63	62	rexlimdvva 3186	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
64	63	adantld 490	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
65	43, 64	biimtrrid 243	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
66	39, 65	sylbid 240	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) → (𝑥𝐻𝑦) ∈ 𝑃))
67	66	ralrimivv 3170	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃)
68	67	ex 412	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐻𝑏) ∈ 𝑃 → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
69	2, 4	igenss 38046	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
70	1, 7, 69	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
71		vex 3440	. . . . . . . . . . . . . . . 16 ⊢ 𝑎 ∈ V
72	71	snss 4736	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝑅 IdlGen {𝑎}) ↔ {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
73	70, 72	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
74	73	adantrr 717	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
75		ssel 3929	. . . . . . . . . . . . 13 ⊢ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → (𝑎 ∈ (𝑅 IdlGen {𝑎}) → 𝑎 ∈ 𝑃))
76	74, 75	syl5com 31	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → 𝑎 ∈ 𝑃))
77	2, 4	igenss 38046	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
78	1, 11, 77	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
79		vex 3440	. . . . . . . . . . . . . . . 16 ⊢ 𝑏 ∈ V
80	79	snss 4736	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝑅 IdlGen {𝑏}) ↔ {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
81	78, 80	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
82	81	adantrl 716	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
83		ssel 3929	. . . . . . . . . . . . 13 ⊢ ((𝑅 IdlGen {𝑏}) ⊆ 𝑃 → (𝑏 ∈ (𝑅 IdlGen {𝑏}) → 𝑏 ∈ 𝑃))
84	82, 83	syl5com 31	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑅 IdlGen {𝑏}) ⊆ 𝑃 → 𝑏 ∈ 𝑃))
85	76, 84	orim12d 966	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))
86	85	adantlr 715	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))
87	68, 86	imim12d 81	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))))
88	26, 87	syld 47	. . . . . . . 8 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))))
89	88	ralrimdvva 3184	. . . . . . 7 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))))
90	89	ex 412	. . . . . 6 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (Idl‘𝑅) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
91	90	adantrd 491	. . . . 5 ⊢ (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
92	91	imdistand 570	. . . 4 ⊢ (𝑅 ∈ CRingOps → (((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))) → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
93		df-3an 1088	. . . 4 ⊢ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))))
94		df-3an 1088	. . . 4 ⊢ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))))
95	92, 93, 94	3imtr4g 296	. . 3 ⊢ (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
96	6, 95	sylbid 240	. 2 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
97	2, 3, 4	ispridl2 38022	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
98	97	ex 412	. . 3 ⊢ (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
99	1, 98	syl 17	. 2 ⊢ (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
100	96, 99	impbid 212	1 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 {cab 2707 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3394 ⊆ wss 3903 {csn 4577 ran crn 5620 ‘cfv 6482 (class class class)co 7349 1^st c1st 7922 2^nd c2nd 7923 RingOpscrngo 37878 CRingOpsccring 37977 Idlcidl 37991 PrIdlcpridl 37992 IdlGen cigen 38043

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-id 5514 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-1st 7924 df-2nd 7925 df-grpo 30437 df-gid 30438 df-ginv 30439 df-ablo 30489 df-ass 37827 df-exid 37829 df-mgmOLD 37833 df-sgrOLD 37845 df-mndo 37851 df-rngo 37879 df-com2 37974 df-crngo 37978 df-idl 37994 df-pridl 37995 df-igen 38044

This theorem is referenced by: pridlc 38055 isdmn3 38058

W3C validator