ssdifidllem

Description: Lemma for ssdifidl : The set P used in the proof of ssdifidl satisfies the condition of Zorn's Lemma. (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)\}$
	ssdifidllem.7	$⊢ φ \to Z \subseteq P$
	ssdifidllem.8	$⊢ φ \to Z \neq \emptyset$
	ssdifidllem.9	$⊢ φ \to [\subset] Or Z$
Assertion	ssdifidllem	$⊢ φ \to ⋃ Z \in P$

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		ssdifidllem.7	$⊢ φ \to Z \subseteq P$
8		ssdifidllem.8	$⊢ φ \to Z \neq \emptyset$
9		ssdifidllem.9	$⊢ φ \to [\subset] Or Z$
10		ineq2	$⊢ p = ⋃ Z \to S \cap p = S \cap ⋃ Z$
11	10	eqeq1d	$⊢ p = ⋃ Z \to (S \cap p = \emptyset \leftrightarrow S \cap ⋃ Z = \emptyset)$
12		sseq2	$⊢ p = ⋃ Z \to (I \subseteq p \leftrightarrow I \subseteq ⋃ Z)$
13	11 12	anbi12d	$⊢ p = ⋃ Z \to ((S \cap p = \emptyset \land I \subseteq p) \leftrightarrow (S \cap ⋃ Z = \emptyset \land I \subseteq ⋃ Z))$
14	6	ssrab3	$⊢ P \subseteq LIdeal (R)$
15	7 14	sstrdi	$⊢ φ \to Z \subseteq LIdeal (R)$
16	15	sselda	$⊢ (φ \land j \in Z) \to j \in LIdeal (R)$
17		eqid	$⊢ LIdeal (R) = LIdeal (R)$
18	1 17	lidlss	$⊢ j \in LIdeal (R) \to j \subseteq B$
19	16 18	syl	$⊢ (φ \land j \in Z) \to j \subseteq B$
20	19	ralrimiva	$⊢ φ \to \forall j \in Z j \subseteq B$
21		unissb	$⊢ ⋃ Z \subseteq B \leftrightarrow \forall j \in Z j \subseteq B$
22	20 21	sylibr	$⊢ φ \to ⋃ Z \subseteq B$
23		eqid	$⊢ 0_{R} = 0_{R}$
24	17 23	lidl0cl	$⊢ (R \in Ring \land j \in LIdeal (R)) \to 0_{R} \in j$
25	2 16 24	syl2an2r	$⊢ (φ \land j \in Z) \to 0_{R} \in j$
26		n0i	$⊢ 0_{R} \in j \to \neg j = \emptyset$
27	25 26	syl	$⊢ (φ \land j \in Z) \to \neg j = \emptyset$
28	27	reximdva0	$⊢ (φ \land Z \neq \emptyset) \to \exists j \in Z \neg j = \emptyset$
29	8 28	mpdan	$⊢ φ \to \exists j \in Z \neg j = \emptyset$
30		rexnal	$⊢ \exists j \in Z \neg j = \emptyset \leftrightarrow \neg \forall j \in Z j = \emptyset$
31	29 30	sylib	$⊢ φ \to \neg \forall j \in Z j = \emptyset$
32		uni0c	$⊢ ⋃ Z = \emptyset \leftrightarrow \forall j \in Z j = \emptyset$
33	32	necon3abii	$⊢ ⋃ Z \neq \emptyset \leftrightarrow \neg \forall j \in Z j = \emptyset$
34	31 33	sylibr	$⊢ φ \to ⋃ Z \neq \emptyset$
35		eluni2	$⊢ a \in ⋃ Z \leftrightarrow \exists i \in Z a \in i$
36		eluni2	$⊢ b \in ⋃ Z \leftrightarrow \exists j \in Z b \in j$
37	35 36	anbi12i	$⊢ (a \in ⋃ Z \land b \in ⋃ Z) \leftrightarrow (\exists i \in Z a \in i \land \exists j \in Z b \in j)$
38		an32	$⊢ (((φ \land x \in B) \land \exists i \in Z a \in i) \land j \in Z) \leftrightarrow (((φ \land x \in B) \land j \in Z) \land \exists i \in Z a \in i)$
39	2	ad6antr	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to R \in Ring$
40	15	ad6antr	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to Z \subseteq LIdeal (R)$
41		simp-5r	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to j \in Z$
42	40 41	sseldd	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to j \in LIdeal (R)$
43		eqid	$⊢ \cdot_{R} = \cdot_{R}$
44		simp-6r	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to x \in B$
45		simpr	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to i \subseteq j$
46		simplr	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to a \in i$
47	45 46	sseldd	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to a \in j$
48	17 1 43 39 42 44 47	lidlmcld	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to x \cdot_{R} a \in j$
49		simp-4r	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to b \in j$
50		eqid	$⊢ +_{R} = +_{R}$
51	17 50	lidlacl	$⊢ ((R \in Ring \land j \in LIdeal (R)) \land (x \cdot_{R} a \in j \land b \in j)) \to (x \cdot_{R} a) +_{R} b \in j$
52	39 42 48 49 51	syl22anc	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to (x \cdot_{R} a) +_{R} b \in j$
53		elunii	$⊢ ((x \cdot_{R} a) +_{R} b \in j \land j \in Z) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
54	52 41 53	syl2anc	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land i \subseteq j) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
55	2	ad6antr	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to R \in Ring$
56	15	ad6antr	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to Z \subseteq LIdeal (R)$
57		simpllr	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to i \in Z$
58	56 57	sseldd	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to i \in LIdeal (R)$
59		simp-6r	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to x \in B$
60		simplr	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to a \in i$
61	17 1 43 55 58 59 60	lidlmcld	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to x \cdot_{R} a \in i$
62		simpr	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to j \subseteq i$
63		simp-4r	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to b \in j$
64	62 63	sseldd	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to b \in i$
65	17 50	lidlacl	$⊢ ((R \in Ring \land i \in LIdeal (R)) \land (x \cdot_{R} a \in i \land b \in i)) \to (x \cdot_{R} a) +_{R} b \in i$
66	55 58 61 64 65	syl22anc	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to (x \cdot_{R} a) +_{R} b \in i$
67		elunii	$⊢ ((x \cdot_{R} a) +_{R} b \in i \land i \in Z) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
68	66 57 67	syl2anc	$⊢ ((((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \land j \subseteq i) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
69	9	ad5antr	$⊢ (((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \to [\subset] Or Z$
70		simplr	$⊢ (((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \to i \in Z$
71		simp-4r	$⊢ (((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \to j \in Z$
72		sorpssi	$⊢ ([\subset] Or Z \land (i \in Z \land j \in Z)) \to (i \subseteq j \lor j \subseteq i)$
73	69 70 71 72	syl12anc	$⊢ (((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \to (i \subseteq j \lor j \subseteq i)$
74	54 68 73	mpjaodan	$⊢ (((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
75	74	r19.29an	$⊢ ((((φ \land x \in B) \land j \in Z) \land b \in j) \land \exists i \in Z a \in i) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
76	75	an32s	$⊢ ((((φ \land x \in B) \land j \in Z) \land \exists i \in Z a \in i) \land b \in j) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
77	38 76	sylanb	$⊢ ((((φ \land x \in B) \land \exists i \in Z a \in i) \land j \in Z) \land b \in j) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
78	77	r19.29an	$⊢ (((φ \land x \in B) \land \exists i \in Z a \in i) \land \exists j \in Z b \in j) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
79	78	anasss	$⊢ ((φ \land x \in B) \land (\exists i \in Z a \in i \land \exists j \in Z b \in j)) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
80	37 79	sylan2b	$⊢ ((φ \land x \in B) \land (a \in ⋃ Z \land b \in ⋃ Z)) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
81	80	ralrimivva	$⊢ (φ \land x \in B) \to \forall a \in ⋃ Z \forall b \in ⋃ Z (x \cdot_{R} a) +_{R} b \in ⋃ Z$
82	81	ralrimiva	$⊢ φ \to \forall x \in B \forall a \in ⋃ Z \forall b \in ⋃ Z (x \cdot_{R} a) +_{R} b \in ⋃ Z$
83	17 1 50 43	islidl	$⊢ ⋃ Z \in LIdeal (R) \leftrightarrow (⋃ Z \subseteq B \land ⋃ Z \neq \emptyset \land \forall x \in B \forall a \in ⋃ Z \forall b \in ⋃ Z (x \cdot_{R} a) +_{R} b \in ⋃ Z)$
84	22 34 82 83	syl3anbrc	$⊢ φ \to ⋃ Z \in LIdeal (R)$
85		iunss1	$⊢ Z \subseteq P \to ⋃_{j \in Z} (S \cap j) \subseteq ⋃_{j \in P} (S \cap j)$
86	7 85	syl	$⊢ φ \to ⋃_{j \in Z} (S \cap j) \subseteq ⋃_{j \in P} (S \cap j)$
87		uniin2	$⊢ ⋃_{j \in Z} (S \cap j) = S \cap ⋃ Z$
88	87	a1i	$⊢ φ \to ⋃_{j \in Z} (S \cap j) = S \cap ⋃ Z$
89	14	a1i	$⊢ φ \to P \subseteq LIdeal (R)$
90	89	sselda	$⊢ (φ \land j \in P) \to j \in LIdeal (R)$
91		simpr	$⊢ (φ \land j \in P) \to j \in P$
92	91 6	eleqtrdi	$⊢ (φ \land j \in P) \to j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land I \subseteq p)\}$
93		ineq2	$⊢ p = j \to S \cap p = S \cap j$
94	93	eqeq1d	$⊢ p = j \to (S \cap p = \emptyset \leftrightarrow S \cap j = \emptyset)$
95		sseq2	$⊢ p = j \to (I \subseteq p \leftrightarrow I \subseteq j)$
96	94 95	anbi12d	$⊢ p = j \to ((S \cap p = \emptyset \land I \subseteq p) \leftrightarrow (S \cap j = \emptyset \land I \subseteq j))$
97	96	elrab3	$⊢ j \in LIdeal (R) \to (j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land I \subseteq p)\} \leftrightarrow (S \cap j = \emptyset \land I \subseteq j))$
98	97	simprbda	$⊢ (j \in LIdeal (R) \land j \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land I \subseteq p)\}) \to S \cap j = \emptyset$
99	90 92 98	syl2anc	$⊢ (φ \land j \in P) \to S \cap j = \emptyset$
100	99	iuneq2dv	$⊢ φ \to ⋃_{j \in P} (S \cap j) = ⋃_{j \in P} \emptyset$
101		iun0	$⊢ ⋃_{j \in P} \emptyset = \emptyset$
102	100 101	eqtrdi	$⊢ φ \to ⋃_{j \in P} (S \cap j) = \emptyset$
103	86 88 102	3sstr3d	$⊢ φ \to S \cap ⋃ Z \subseteq \emptyset$
104		ss0	$⊢ S \cap ⋃ Z \subseteq \emptyset \to S \cap ⋃ Z = \emptyset$
105	103 104	syl	$⊢ φ \to S \cap ⋃ Z = \emptyset$
106	7	sselda	$⊢ (φ \land j \in Z) \to j \in P$
107	96 6	elrab2	$⊢ j \in P \leftrightarrow (j \in LIdeal (R) \land (S \cap j = \emptyset \land I \subseteq j))$
108	106 107	sylib	$⊢ (φ \land j \in Z) \to (j \in LIdeal (R) \land (S \cap j = \emptyset \land I \subseteq j))$
109	108	simprrd	$⊢ (φ \land j \in Z) \to I \subseteq j$
110	109	ralrimiva	$⊢ φ \to \forall j \in Z I \subseteq j$
111		ssint	$⊢ I \subseteq ⋂ Z \leftrightarrow \forall j \in Z I \subseteq j$
112	110 111	sylibr	$⊢ φ \to I \subseteq ⋂ Z$
113		intssuni	$⊢ Z \neq \emptyset \to ⋂ Z \subseteq ⋃ Z$
114	8 113	syl	$⊢ φ \to ⋂ Z \subseteq ⋃ Z$
115	112 114	sstrd	$⊢ φ \to I \subseteq ⋃ Z$
116	105 115	jca	$⊢ φ \to (S \cap ⋃ Z = \emptyset \land I \subseteq ⋃ Z)$
117	13 84 116	elrabd	$⊢ φ \to ⋃ Z \in \{p \in LIdeal (R) \| (S \cap p = \emptyset \land I \subseteq p)\}$
118	117 6	eleqtrrdi	$⊢ φ \to ⋃ Z \in P$

Metamath Proof Explorer

Theorem ssdifidllem

Proof