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 38408

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 38338	. . . 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 38372	. . . 4 ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
6	1, 5	syl 17	. . 3 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
7		snssi 4752	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑋 → {𝑎} ⊆ 𝑋)
8	2, 4	igenidl 38401	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
9	1, 7, 8	syl2an 597	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
10	9	adantrr 718	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
11		snssi 4752	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝑋 → {𝑏} ⊆ 𝑋)
12	2, 4	igenidl 38401	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
13	1, 11, 12	syl2an 597	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
14	13	adantrl 717	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
15		raleq 3293	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃))
16		sseq1 3948	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (𝑟 ⊆ 𝑃 ↔ (𝑅 IdlGen {𝑎}) ⊆ 𝑃))
17	16	orbi1d 917	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))
18	15, 17	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))))
19		raleq 3293	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
20	19	ralbidv 3161	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
21		sseq1 3948	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (𝑠 ⊆ 𝑃 ↔ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))
22	21	orbi2d 916	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)))
23	20, 22	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
24	18, 23	rspc2v 3576	. . . . . . . . . . 11 ⊢ (((𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅) ∧ (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
25	10, 14, 24	syl2anc 585	. . . . . . . . . 10 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
26	25	adantlr 716	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
27	2, 3, 4	prnc 38405	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)})
28		df-rab 3391	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)} = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))}
29	27, 28	eqtrdi 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))})
30	29	eqabrd 2878	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
31	30	adantrr 718	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
32	2, 3, 4	prnc 38405	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)})
33		df-rab 3391	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)} = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))}
34	32, 33	eqtrdi 2788	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))})
35	34	eqabrd 2878	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
36	35	adantrl 717	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
37	31, 36	anbi12d 633	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))))
38	37	adantlr 716	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))))
39	38	adantr 480	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))))
40		reeanv 3210	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) ↔ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))
41	40	anbi2i 624	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
42		an4 657	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
43	41, 42	bitri 275	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
44	2, 3, 4	crngm4 38341	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
45	44	3com23 1127	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
46	45	3expa 1119	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
47	46	adantllr 720	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
48	47	adantlr 716	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
49	2, 3, 4	rngocl 38239	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
50	1, 49	syl3an1 1164	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
51	50	3expb 1121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
52	51	adantlr 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
53	52	adantlr 716	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
54	2, 3, 4	idllmulcl 38358	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
55	1, 54	sylanl1 681	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
56	55	anassrs 467	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝐻𝑠) ∈ 𝑋) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
57	53, 56	syldan 592	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
58	57	adantllr 720	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
59	48, 58	eqeltrrd 2838	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃)
60		oveq12 7370	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
61	60	eleq1d 2822	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → ((𝑥𝐻𝑦) ∈ 𝑃 ↔ ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃))
62	59, 61	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
63	62	rexlimdvva 3195	. . . . . . . . . . . . . . 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 3179	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃)
68	67	ex 412	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐻𝑏) ∈ 𝑃 → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
69	2, 4	igenss 38400	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
70	1, 7, 69	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
71		vex 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑎 ∈ V
72	71	snss 4729	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝑅 IdlGen {𝑎}) ↔ {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
73	70, 72	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
74	73	adantrr 718	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
75		ssel 3916	. . . . . . . . . . . . 13 ⊢ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → (𝑎 ∈ (𝑅 IdlGen {𝑎}) → 𝑎 ∈ 𝑃))
76	74, 75	syl5com 31	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → 𝑎 ∈ 𝑃))
77	2, 4	igenss 38400	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
78	1, 11, 77	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
79		vex 3434	. . . . . . . . . . . . . . . 16 ⊢ 𝑏 ∈ V
80	79	snss 4729	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝑅 IdlGen {𝑏}) ↔ {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
81	78, 80	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
82	81	adantrl 717	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
83		ssel 3916	. . . . . . . . . . . . 13 ⊢ ((𝑅 IdlGen {𝑏}) ⊆ 𝑃 → (𝑏 ∈ (𝑅 IdlGen {𝑏}) → 𝑏 ∈ 𝑃))
84	82, 83	syl5com 31	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑅 IdlGen {𝑏}) ⊆ 𝑃 → 𝑏 ∈ 𝑃))
85	76, 84	orim12d 967	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))
86	85	adantlr 716	. . . . . . . . . 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 3193	. . . . . . 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 1089	. . . 4 ⊢ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))))
94		df-3an 1089	. . . 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 38376	. . . 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 848 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 {cab 2715 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 {crab 3390 ⊆ wss 3890 {csn 4568 ran crn 5626 ‘cfv 6493 (class class class)co 7361 1^st c1st 7934 2^nd c2nd 7935 RingOpscrngo 38232 CRingOpsccring 38331 Idlcidl 38345 PrIdlcpridl 38346 IdlGen cigen 38397

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 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5303 ax-pr 5371 ax-un 7683

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-iota 6449 df-fun 6495 df-fn 6496 df-f 6497 df-f1 6498 df-fo 6499 df-f1o 6500 df-fv 6501 df-riota 7318 df-ov 7364 df-oprab 7365 df-mpo 7366 df-1st 7936 df-2nd 7937 df-grpo 30582 df-gid 30583 df-ginv 30584 df-ablo 30634 df-ass 38181 df-exid 38183 df-mgmOLD 38187 df-sgrOLD 38199 df-mndo 38205 df-rngo 38233 df-com2 38328 df-crngo 38332 df-idl 38348 df-pridl 38349 df-igen 38398

This theorem is referenced by: pridlc 38409 isdmn3 38412

W3C validator