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 38099

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 38029	. . . 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 38063	. . . 4 ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
6	1, 5	syl 17	. . 3 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
7		snssi 4789	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑋 → {𝑎} ⊆ 𝑋)
8	2, 4	igenidl 38092	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
9	1, 7, 8	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
10	9	adantrr 717	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
11		snssi 4789	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝑋 → {𝑏} ⊆ 𝑋)
12	2, 4	igenidl 38092	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
13	1, 11, 12	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
14	13	adantrl 716	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
15		raleq 3306	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃))
16		sseq1 3989	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (𝑟 ⊆ 𝑃 ↔ (𝑅 IdlGen {𝑎}) ⊆ 𝑃))
17	16	orbi1d 916	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))
18	15, 17	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))))
19		raleq 3306	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
20	19	ralbidv 3164	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
21		sseq1 3989	. . . . . . . . . . . . . 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 3617	. . . . . . . . . . 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 38096	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)})
28		df-rab 3421	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)} = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))}
29	27, 28	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))})
30	29	eqabrd 2878	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
31	30	adantrr 717	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
32	2, 3, 4	prnc 38096	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)})
33		df-rab 3421	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)} = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))}
34	32, 33	eqtrdi 2787	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))})
35	34	eqabrd 2878	. . . . . . . . . . . . . . . . 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 3217	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) ↔ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))
41	40	anbi2i 623	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
42		an4 656	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
43	41, 42	bitri 275	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
44	2, 3, 4	crngm4 38032	. . . . . . . . . . . . . . . . . . . . . 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 37930	. . . . . . . . . . . . . . . . . . . . . . . 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 38049	. . . . . . . . . . . . . . . . . . . . . 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 2836	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃)
60		oveq12 7419	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
61	60	eleq1d 2820	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → ((𝑥𝐻𝑦) ∈ 𝑃 ↔ ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃))
62	59, 61	syl5ibrcom 247	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
63	62	rexlimdvva 3202	. . . . . . . . . . . . . . 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 3186	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃)
68	67	ex 412	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐻𝑏) ∈ 𝑃 → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
69	2, 4	igenss 38091	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
70	1, 7, 69	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
71		vex 3468	. . . . . . . . . . . . . . . 16 ⊢ 𝑎 ∈ V
72	71	snss 4766	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝑅 IdlGen {𝑎}) ↔ {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
73	70, 72	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
74	73	adantrr 717	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
75		ssel 3957	. . . . . . . . . . . . 13 ⊢ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → (𝑎 ∈ (𝑅 IdlGen {𝑎}) → 𝑎 ∈ 𝑃))
76	74, 75	syl5com 31	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → 𝑎 ∈ 𝑃))
77	2, 4	igenss 38091	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
78	1, 11, 77	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
79		vex 3468	. . . . . . . . . . . . . . . 16 ⊢ 𝑏 ∈ V
80	79	snss 4766	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝑅 IdlGen {𝑏}) ↔ {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
81	78, 80	sylibr 234	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
82	81	adantrl 716	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
83		ssel 3957	. . . . . . . . . . . . 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 3200	. . . . . . 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 38067	. . . 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 2714 ≠ wne 2933 ∀wral 3052 ∃wrex 3061 {crab 3420 ⊆ wss 3931 {csn 4606 ran crn 5660 ‘cfv 6536 (class class class)co 7410 1^st c1st 7991 2^nd c2nd 7992 RingOpscrngo 37923 CRingOpsccring 38022 Idlcidl 38036 PrIdlcpridl 38037 IdlGen cigen 38088

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 2708 ax-rep 5254 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734

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 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-int 4928 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-id 5553 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-1st 7993 df-2nd 7994 df-grpo 30479 df-gid 30480 df-ginv 30481 df-ablo 30531 df-ass 37872 df-exid 37874 df-mgmOLD 37878 df-sgrOLD 37890 df-mndo 37896 df-rngo 37924 df-com2 38019 df-crngo 38023 df-idl 38039 df-pridl 38040 df-igen 38089

This theorem is referenced by: pridlc 38100 isdmn3 38103

W3C validator