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 38828

Description: Obsolete theorem, use isprmidlc 21541 instead. The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) (New usage is discouraged.) (Proof modification is discouraged.)

**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 38758	. . . 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 38792	. . . 4 ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
6	1, 5	syl 18	. . 3 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
7		snssi 4749	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑋 → {𝑎} ⊆ 𝑋)
8	2, 4	igenidl 38821	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
9	1, 7, 8	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
10	9	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
11		snssi 4749	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝑋 → {𝑏} ⊆ 𝑋)
12	2, 4	igenidl 38821	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
13	1, 11, 12	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
14	13	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
15		raleq 3318	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃))
16		sseq1 3959	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (𝑟 ⊆ 𝑃 ↔ (𝑅 IdlGen {𝑎}) ⊆ 𝑃))
17	16	orbi1d 930	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))
18	15, 17	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))))
19		raleq 3318	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
20	19	ralbidv 3187	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
21		sseq1 3959	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (𝑠 ⊆ 𝑃 ↔ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))
22	21	orbi2d 929	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)))
23	20, 22	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
24	18, 23	rspc2v 3590	. . . . . . . . . . 11 ⊢ (((𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅) ∧ (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
25	10, 14, 24	syl2anc 596	. . . . . . . . . 10 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
26	25	adantlr 728	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃))))
27	2, 3, 4	prnc 38825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)})
28		df-rab 3415	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)} = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))}
29	27, 28	eqtrdi 2813	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))})
30	29	eqabrd 2903	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
31	30	adantrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
32	2, 3, 4	prnc 38825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)})
33		df-rab 3415	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)} = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))}
34	32, 33	eqtrdi 2813	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))})
35	34	eqabrd 2903	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
36	35	adantrl 729	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑦 ∈ (𝑅 IdlGen {𝑏}) ↔ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
37	31, 36	anbi12d 644	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))))
38	37	adantlr 728	. . . . . . . . . . . . . 14 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))))
39	38	adantr 486	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))))
40		reeanv 3236	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) ↔ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))
41	40	anbi2i 635	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
42		an4 669	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
43	41, 42	bitri 278	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
44	2, 3, 4	crngm4 38761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
45	44	3com23 1144	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
46	45	3expa 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
47	46	adantllr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
48	47	adantlr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
49	2, 3, 4	rngocl 38659	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ RingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
50	1, 49	syl3an1 1181	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑟𝐻𝑠) ∈ 𝑋)
51	50	3expb 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
52	51	adantlr 728	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
53	52	adantlr 728	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → (𝑟𝐻𝑠) ∈ 𝑋)
54	2, 3, 4	idllmulcl 38778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
55	1, 54	sylanl1 693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ ((𝑎𝐻𝑏) ∈ 𝑃 ∧ (𝑟𝐻𝑠) ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
56	55	anassrs 473	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟𝐻𝑠) ∈ 𝑋) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
57	53, 56	syldan 603	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
58	57	adantllr 732	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑠)𝐻(𝑎𝐻𝑏)) ∈ 𝑃)
59	48, 58	eqeltrrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃)
60		oveq12 7426	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
61	60	eleq1d 2847	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → ((𝑥𝐻𝑦) ∈ 𝑃 ↔ ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃))
62	59, 61	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
63	62	rexlimdvva 3221	. . . . . . . . . . . . . . 15 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
64	63	adantld 496	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
65	43, 64	biimtrrid 246	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → (((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))) → (𝑥𝐻𝑦) ∈ 𝑃))
66	39, 65	sylbid 243	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ((𝑥 ∈ (𝑅 IdlGen {𝑎}) ∧ 𝑦 ∈ (𝑅 IdlGen {𝑏})) → (𝑥𝐻𝑦) ∈ 𝑃))
67	66	ralrimivv 3205	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃)
68	67	ex 418	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐻𝑏) ∈ 𝑃 → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
69	2, 4	igenss 38820	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
70	1, 7, 69	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
71		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑎 ∈ V
72	71	snss 4748	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝑅 IdlGen {𝑎}) ↔ {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
73	70, 72	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
74	73	adantrr 730	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
75		ssel 3928	. . . . . . . . . . . . 13 ⊢ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → (𝑎 ∈ (𝑅 IdlGen {𝑎}) → 𝑎 ∈ 𝑃))
76	74, 75	syl5com 32	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → 𝑎 ∈ 𝑃))
77	2, 4	igenss 38820	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
78	1, 11, 77	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
79		vex 3457	. . . . . . . . . . . . . . . 16 ⊢ 𝑏 ∈ V
80	79	snss 4748	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝑅 IdlGen {𝑏}) ↔ {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
81	78, 80	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
82	81	adantrl 729	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
83		ssel 3928	. . . . . . . . . . . . 13 ⊢ ((𝑅 IdlGen {𝑏}) ⊆ 𝑃 → (𝑏 ∈ (𝑅 IdlGen {𝑏}) → 𝑏 ∈ 𝑃))
84	82, 83	syl5com 32	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑅 IdlGen {𝑏}) ⊆ 𝑃 → 𝑏 ∈ 𝑃))
85	76, 84	orim12d 979	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))
86	85	adantlr 728	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃) → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))
87	68, 86	imim12d 82	. . . . . . . . 9 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ (𝑅 IdlGen {𝑏}) ⊆ 𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))))
88	26, 87	syld 48	. . . . . . . 8 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))))
89	88	ralrimdvva 3219	. . . . . . 7 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))))
90	89	ex 418	. . . . . 6 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (Idl‘𝑅) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
91	90	adantrd 497	. . . . 5 ⊢ (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) → (∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
92	91	imdistand 581	. . . 4 ⊢ (𝑅 ∈ CRingOps → (((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))) → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
93		df-3an 1105	. . . 4 ⊢ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))))
94		df-3an 1105	. . . 4 ⊢ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))) ↔ ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))))
95	92, 93, 94	3imtr4g 299	. . 3 ⊢ (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
96	6, 95	sylbid 243	. 2 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) → (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))
97	2, 3, 4	ispridl2 38796	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅))
98	97	ex 418	. . 3 ⊢ (𝑅 ∈ RingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
99	1, 98	syl 18	. 2 ⊢ (𝑅 ∈ CRingOps → ((𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃))) → 𝑃 ∈ (PrIdl‘𝑅)))
100	96, 99	impbid 215	1 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 {cab 2740 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 {crab 3414 ⊆ wss 3902 {csn 4587 ran crn 5660 ‘cfv 6537 (class class class)co 7417 1^st c1st 7988 2^nd c2nd 7989 RingOpscrngo 38652 CRingOpsccring 38751 Idlcidl 38765 PrIdlcpridl 38766 IdlGen cigen 38817

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-br 5108 df-opab 5172 df-mpt 5191 df-id 5554 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 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-1st 7990 df-2nd 7991 df-grpo 30982 df-gid 30983 df-ginv 30984 df-ablo 31034 df-ass 38601 df-exid 38603 df-mgmOLD 38607 df-sgrOLD 38619 df-mndo 38625 df-rngo 38653 df-com2 38748 df-crngo 38752 df-idl 38768 df-pridl 38769 df-igen 38818

This theorem is used by: pridlc 38829 isdmn3 38832

W3C validator