ssdifidl

Description: Let R be a ring, and let I be an ideal of R disjoint with a set S . Then there exists an ideal i , maximal among the set P of ideals containing I and disjoint with S . (Contributed by Thierry Arnoux, 3-Jun-2025)

	Ref	Expression
Hypotheses	ssdifidl.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ssdifidl.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	ssdifidl.3	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
	ssdifidl.4	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
	ssdifidl.5	⊢ ( 𝜑 → ( 𝑆 ∩ 𝐼 ) = ∅ )
	ssdifidl.6	⊢ 𝑃 = { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ 𝐼 ⊆ 𝑝 ) }
Assertion	ssdifidl	⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝑃 ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 )

Proof

Step	Hyp	Ref	Expression
1		ssdifidl.1	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		ssdifidl.2	⊢ ( 𝜑 → 𝑅 ∈ Ring )
3		ssdifidl.3	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
4		ssdifidl.4	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
5		ssdifidl.5	⊢ ( 𝜑 → ( 𝑆 ∩ 𝐼 ) = ∅ )
6		ssdifidl.6	⊢ 𝑃 = { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ 𝐼 ⊆ 𝑝 ) }
7		ineq2	⊢ ( 𝑝 = 𝐼 → ( 𝑆 ∩ 𝑝 ) = ( 𝑆 ∩ 𝐼 ) )
8	7	eqeq1d	⊢ ( 𝑝 = 𝐼 → ( ( 𝑆 ∩ 𝑝 ) = ∅ ↔ ( 𝑆 ∩ 𝐼 ) = ∅ ) )
9		sseq2	⊢ ( 𝑝 = 𝐼 → ( 𝐼 ⊆ 𝑝 ↔ 𝐼 ⊆ 𝐼 ) )
10	8 9	anbi12d	⊢ ( 𝑝 = 𝐼 → ( ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ 𝐼 ⊆ 𝑝 ) ↔ ( ( 𝑆 ∩ 𝐼 ) = ∅ ∧ 𝐼 ⊆ 𝐼 ) ) )
11		ssidd	⊢ ( 𝜑 → 𝐼 ⊆ 𝐼 )
12	5 11	jca	⊢ ( 𝜑 → ( ( 𝑆 ∩ 𝐼 ) = ∅ ∧ 𝐼 ⊆ 𝐼 ) )
13	10 3 12	elrabd	⊢ ( 𝜑 → 𝐼 ∈ { 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∣ ( ( 𝑆 ∩ 𝑝 ) = ∅ ∧ 𝐼 ⊆ 𝑝 ) } )
14	13 6	eleqtrrdi	⊢ ( 𝜑 → 𝐼 ∈ 𝑃 )
15	14	ne0d	⊢ ( 𝜑 → 𝑃 ≠ ∅ )
16	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝑅 ∈ Ring )
17	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )
18	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝑆 ⊆ 𝐵 )
19	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → ( 𝑆 ∩ 𝐼 ) = ∅ )
20		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝑧 ⊆ 𝑃 )
21		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → 𝑧 ≠ ∅ )
22		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → [⊊] Or 𝑧 )
23	1 16 17 18 19 6 20 21 22	ssdifidllem	⊢ ( ( 𝜑 ∧ ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) ) → ∪ 𝑧 ∈ 𝑃 )
24	23	ex	⊢ ( 𝜑 → ( ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝑃 ) )
25	24	alrimiv	⊢ ( 𝜑 → ∀ 𝑧 ( ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝑃 ) )
26		fvex	⊢ ( LIdeal ‘ 𝑅 ) ∈ V
27	6 26	rabex2	⊢ 𝑃 ∈ V
28	27	zornn0	⊢ ( ( 𝑃 ≠ ∅ ∧ ∀ 𝑧 ( ( 𝑧 ⊆ 𝑃 ∧ 𝑧 ≠ ∅ ∧ [⊊] Or 𝑧 ) → ∪ 𝑧 ∈ 𝑃 ) ) → ∃ 𝑖 ∈ 𝑃 ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 )
29	15 25 28	syl2anc	⊢ ( 𝜑 → ∃ 𝑖 ∈ 𝑃 ∀ 𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗 )

Metamath Proof Explorer

Theorem ssdifidl

Proof