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	$⊢ B = {Base}_{R}$
	ssdifidl.2	$⊢ φ \to R \in Ring$
	ssdifidl.3	$⊢ φ \to I \in LIdeal (R)$
	ssdifidl.4	$⊢ φ \to S \subseteq B$
	ssdifidl.5	$⊢ φ \to S \cap I = \emptyset$
	ssdifidl.6	$⊢ P = \{p \in LIdeal (R) \| (S \cap p = \emptyset \land I \subseteq p)\}$
Assertion	ssdifidl	$⊢ φ \to \exists i \in P \forall j \in P \neg i \subset j$

Proof

Step	Hyp	Ref	Expression
1		ssdifidl.1	$⊢ B = {Base}_{R}$
2		ssdifidl.2	$⊢ φ \to R \in Ring$
3		ssdifidl.3	$⊢ φ \to I \in LIdeal (R)$
4		ssdifidl.4	$⊢ φ \to S \subseteq B$
5		ssdifidl.5	$⊢ φ \to S \cap I = \emptyset$
6		ssdifidl.6	$⊢ P = \{p \in LIdeal (R) \| (S \cap p = \emptyset \land I \subseteq p)\}$
7		ineq2	$⊢ p = I \to S \cap p = S \cap I$
8	7	eqeq1d	$⊢ p = I \to (S \cap p = \emptyset \leftrightarrow S \cap I = \emptyset)$
9		sseq2	$⊢ p = I \to (I \subseteq p \leftrightarrow I \subseteq I)$
10	8 9	anbi12d	$⊢ p = I \to ((S \cap p = \emptyset \land I \subseteq p) \leftrightarrow (S \cap I = \emptyset \land I \subseteq I))$
11		ssidd	$⊢ φ \to I \subseteq I$
12	5 11	jca	$⊢ φ \to (S \cap I = \emptyset \land I \subseteq I)$
13	10 3 12	elrabd	$⊢ φ \to I \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land I \subseteq p)\}$
14	13 6	eleqtrrdi	$⊢ φ \to I \in P$
15	14	ne0d	$⊢ φ \to P \neq \emptyset$
16	2	adantr	$⊢ (φ \land (z \subseteq P \land z \neq \emptyset \land [\subset] Or z)) \to R \in Ring$
17	3	adantr	$⊢ (φ \land (z \subseteq P \land z \neq \emptyset \land [\subset] Or z)) \to I \in LIdeal (R)$
18	4	adantr	$⊢ (φ \land (z \subseteq P \land z \neq \emptyset \land [\subset] Or z)) \to S \subseteq B$
19	5	adantr	$⊢ (φ \land (z \subseteq P \land z \neq \emptyset \land [\subset] Or z)) \to S \cap I = \emptyset$
20		simpr1	$⊢ (φ \land (z \subseteq P \land z \neq \emptyset \land [\subset] Or z)) \to z \subseteq P$
21		simpr2	$⊢ (φ \land (z \subseteq P \land z \neq \emptyset \land [\subset] Or z)) \to z \neq \emptyset$
22		simpr3	$⊢ (φ \land (z \subseteq P \land z \neq \emptyset \land [\subset] Or z)) \to [\subset] Or z$
23	1 16 17 18 19 6 20 21 22	ssdifidllem	$⊢ (φ \land (z \subseteq P \land z \neq \emptyset \land [\subset] Or z)) \to ⋃ z \in P$
24	23	ex	$⊢ φ \to ((z \subseteq P \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in P)$
25	24	alrimiv	$⊢ φ \to \forall z ((z \subseteq P \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in P)$
26		fvex	$⊢ LIdeal (R) \in V$
27	6 26	rabex2	$⊢ P \in V$
28	27	zornn0	$⊢ (P \neq \emptyset \land \forall z ((z \subseteq P \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in P)) \to \exists i \in P \forall j \in P \neg i \subset j$
29	15 25 28	syl2anc	$⊢ φ \to \exists i \in P \forall j \in P \neg i \subset j$

Metamath Proof Explorer

Theorem ssdifidl

Proof