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 38781

Description: Obsolete theorem, use isprmidlc 21524 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 38711	. . . 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 38745	. . . 4 ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
6	1, 5	syl 18	. . 3 ⊢ (𝑅 ∈ CRingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑟 ∈ (Idl‘𝑅)∀𝑠 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))))
7		snssi 4753	. . . . . . . . . . . . 13 ⊢ (𝑎 ∈ 𝑋 → {𝑎} ⊆ 𝑋)
8	2, 4	igenidl 38774	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
9	1, 7, 8	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
10	9	adantrr 730	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑎}) ∈ (Idl‘𝑅))
11		snssi 4753	. . . . . . . . . . . . 13 ⊢ (𝑏 ∈ 𝑋 → {𝑏} ⊆ 𝑋)
12	2, 4	igenidl 38774	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
13	1, 11, 12	syl2an 608	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
14	13	adantrl 729	. . . . . . . . . . 11 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑅 IdlGen {𝑏}) ∈ (Idl‘𝑅))
15		raleq 3322	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃))
16		sseq1 3963	. . . . . . . . . . . . . 14 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → (𝑟 ⊆ 𝑃 ↔ (𝑅 IdlGen {𝑎}) ⊆ 𝑃))
17	16	orbi1d 930	. . . . . . . . . . . . 13 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃) ↔ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)))
18	15, 17	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑟 = (𝑅 IdlGen {𝑎}) → ((∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑟 ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃)) ↔ (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 ∨ 𝑠 ⊆ 𝑃))))
19		raleq 3322	. . . . . . . . . . . . . 14 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
20	19	ralbidv 3190	. . . . . . . . . . . . 13 ⊢ (𝑠 = (𝑅 IdlGen {𝑏}) → (∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ 𝑠 (𝑥𝐻𝑦) ∈ 𝑃 ↔ ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
21		sseq1 3963	. . . . . . . . . . . . . 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 3594	. . . . . . . . . . 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 38778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)})
28		df-rab 3419	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑥 ∈ 𝑋 ∣ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)} = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))}
29	27, 28	eqtrdi 2816	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑅 IdlGen {𝑎}) = {𝑥 ∣ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))})
30	29	eqabrd 2906	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
31	30	adantrr 730	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑥 ∈ (𝑅 IdlGen {𝑎}) ↔ (𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎))))
32	2, 3, 4	prnc 38778	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)})
33		df-rab 3419	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ 𝑋 ∣ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)} = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))}
34	32, 33	eqtrdi 2816	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → (𝑅 IdlGen {𝑏}) = {𝑦 ∣ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))})
35	34	eqabrd 2906	. . . . . . . . . . . . . . . . 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 3239	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) ↔ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏)))
41	40	anbi2i 635	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
42		an4 669	. . . . . . . . . . . . . . 15 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ (∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎) ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
43	41, 42	bitri 278	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) ∧ ∃𝑟 ∈ 𝑋 ∃𝑠 ∈ 𝑋 (𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏))) ↔ ((𝑥 ∈ 𝑋 ∧ ∃𝑟 ∈ 𝑋 𝑥 = (𝑟𝐻𝑎)) ∧ (𝑦 ∈ 𝑋 ∧ ∃𝑠 ∈ 𝑋 𝑦 = (𝑠𝐻𝑏))))
44	2, 3, 4	crngm4 38714	. . . . . . . . . . . . . . . . . . . . . 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 38612	. . . . . . . . . . . . . . . . . . . . . . . 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 38731	. . . . . . . . . . . . . . . . . . . . . 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 2866	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃)
60		oveq12 7428	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) = ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)))
61	60	eleq1d 2850	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → ((𝑥𝐻𝑦) ∈ 𝑃 ↔ ((𝑟𝐻𝑎)𝐻(𝑠𝐻𝑏)) ∈ 𝑃))
62	59, 61	syl5ibrcom 250	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) ∧ (𝑟 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋)) → ((𝑥 = (𝑟𝐻𝑎) ∧ 𝑦 = (𝑠𝐻𝑏)) → (𝑥𝐻𝑦) ∈ 𝑃))
63	62	rexlimdvva 3224	. . . . . . . . . . . . . . 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 3208	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) ∧ (𝑎𝐻𝑏) ∈ 𝑃) → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃)
68	67	ex 418	. . . . . . . . . 10 ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (Idl‘𝑅)) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐻𝑏) ∈ 𝑃 → ∀𝑥 ∈ (𝑅 IdlGen {𝑎})∀𝑦 ∈ (𝑅 IdlGen {𝑏})(𝑥𝐻𝑦) ∈ 𝑃))
69	2, 4	igenss 38773	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑎} ⊆ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
70	1, 7, 69	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
71		vex 3461	. . . . . . . . . . . . . . . 16 ⊢ 𝑎 ∈ V
72	71	snss 4752	. . . . . . . . . . . . . . 15 ⊢ (𝑎 ∈ (𝑅 IdlGen {𝑎}) ↔ {𝑎} ⊆ (𝑅 IdlGen {𝑎}))
73	70, 72	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑎 ∈ 𝑋) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
74	73	adantrr 730	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑎 ∈ (𝑅 IdlGen {𝑎}))
75		ssel 3932	. . . . . . . . . . . . 13 ⊢ ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → (𝑎 ∈ (𝑅 IdlGen {𝑎}) → 𝑎 ∈ 𝑃))
76	74, 75	syl5com 32	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑅 IdlGen {𝑎}) ⊆ 𝑃 → 𝑎 ∈ 𝑃))
77	2, 4	igenss 38773	. . . . . . . . . . . . . . . 16 ⊢ ((𝑅 ∈ RingOps ∧ {𝑏} ⊆ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
78	1, 11, 77	syl2an 608	. . . . . . . . . . . . . . 15 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
79		vex 3461	. . . . . . . . . . . . . . . 16 ⊢ 𝑏 ∈ V
80	79	snss 4752	. . . . . . . . . . . . . . 15 ⊢ (𝑏 ∈ (𝑅 IdlGen {𝑏}) ↔ {𝑏} ⊆ (𝑅 IdlGen {𝑏}))
81	78, 80	sylibr 237	. . . . . . . . . . . . . 14 ⊢ ((𝑅 ∈ CRingOps ∧ 𝑏 ∈ 𝑋) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
82	81	adantrl 729	. . . . . . . . . . . . 13 ⊢ ((𝑅 ∈ CRingOps ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → 𝑏 ∈ (𝑅 IdlGen {𝑏}))
83		ssel 3932	. . . . . . . . . . . . 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 3222	. . . . . . 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 38749	. . . 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 2146 {cab 2743 ≠ wne 2960 ∀wral 3081 ∃wrex 3091 {crab 3418 ⊆ wss 3906 {csn 4591 ran crn 5664 ‘cfv 6540 (class class class)co 7419 1^st c1st 7990 2^nd c2nd 7991 RingOpscrngo 38605 CRingOpsccring 38704 Idlcidl 38718 PrIdlcpridl 38719 IdlGen cigen 38770

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742

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 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-1st 7992 df-2nd 7993 df-grpo 30918 df-gid 30919 df-ginv 30920 df-ablo 30970 df-ass 38554 df-exid 38556 df-mgmOLD 38560 df-sgrOLD 38572 df-mndo 38578 df-rngo 38606 df-com2 38701 df-crngo 38705 df-idl 38721 df-pridl 38722 df-igen 38771

This theorem is used by: pridlc 38782 isdmn3 38785

W3C validator