ssmxidllem

Description: The set P used in the proof of ssmxidl satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024)

	Ref	Expression
Hypotheses	ssmxidl.1	$⊢ B = {Base}_{R}$
	ssmxidllem.1	$⊢ P = \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\}$
	ssmxidllem.2	$⊢ φ \to R \in Ring$
	ssmxidllem.3	$⊢ φ \to I \in LIdeal (R)$
	ssmxidllem.4	$⊢ φ \to I \neq B$
	ssmxidllem2.1	$⊢ φ \to Z \subseteq P$
	ssmxidllem2.2	$⊢ φ \to Z \neq \emptyset$
	ssmxidllem2.3	$⊢ φ \to [\subset] Or Z$
Assertion	ssmxidllem	$⊢ φ \to ⋃ Z \in P$

Proof

Step	Hyp	Ref	Expression
1		ssmxidl.1	$⊢ B = {Base}_{R}$
2		ssmxidllem.1	$⊢ P = \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\}$
3		ssmxidllem.2	$⊢ φ \to R \in Ring$
4		ssmxidllem.3	$⊢ φ \to I \in LIdeal (R)$
5		ssmxidllem.4	$⊢ φ \to I \neq B$
6		ssmxidllem2.1	$⊢ φ \to Z \subseteq P$
7		ssmxidllem2.2	$⊢ φ \to Z \neq \emptyset$
8		ssmxidllem2.3	$⊢ φ \to [\subset] Or Z$
9		neeq1	$⊢ p = ⋃ Z \to (p \neq B \leftrightarrow ⋃ Z \neq B)$
10		sseq2	$⊢ p = ⋃ Z \to (I \subseteq p \leftrightarrow I \subseteq ⋃ Z)$
11	9 10	anbi12d	$⊢ p = ⋃ Z \to ((p \neq B \land I \subseteq p) \leftrightarrow (⋃ Z \neq B \land I \subseteq ⋃ Z))$
12	2	ssrab3	$⊢ P \subseteq LIdeal (R)$
13	6 12	sstrdi	$⊢ φ \to Z \subseteq LIdeal (R)$
14	13	sselda	$⊢ (φ \land j \in Z) \to j \in LIdeal (R)$
15		eqid	$⊢ LIdeal (R) = LIdeal (R)$
16	1 15	lidlss	$⊢ j \in LIdeal (R) \to j \subseteq B$
17	14 16	syl	$⊢ (φ \land j \in Z) \to j \subseteq B$
18	17	ralrimiva	$⊢ φ \to \forall j \in Z j \subseteq B$
19		unissb	$⊢ ⋃ Z \subseteq B \leftrightarrow \forall j \in Z j \subseteq B$
20	18 19	sylibr	$⊢ φ \to ⋃ Z \subseteq B$
21	3	adantr	$⊢ (φ \land j \in Z) \to R \in Ring$
22		eqid	$⊢ 0_{R} = 0_{R}$
23	15 22	lidl0cl	$⊢ (R \in Ring \land j \in LIdeal (R)) \to 0_{R} \in j$
24	21 14 23	syl2anc	$⊢ (φ \land j \in Z) \to 0_{R} \in j$
25		n0i	$⊢ 0_{R} \in j \to \neg j = \emptyset$
26	24 25	syl	$⊢ (φ \land j \in Z) \to \neg j = \emptyset$
27	26	reximdva0	$⊢ (φ \land Z \neq \emptyset) \to \exists j \in Z \neg j = \emptyset$
28	7 27	mpdan	$⊢ φ \to \exists j \in Z \neg j = \emptyset$
29		rexnal	$⊢ \exists j \in Z \neg j = \emptyset \leftrightarrow \neg \forall j \in Z j = \emptyset$
30	28 29	sylib	$⊢ φ \to \neg \forall j \in Z j = \emptyset$
31		uni0c	$⊢ ⋃ Z = \emptyset \leftrightarrow \forall j \in Z j = \emptyset$
32	31	necon3abii	$⊢ ⋃ Z \neq \emptyset \leftrightarrow \neg \forall j \in Z j = \emptyset$
33	30 32	sylibr	$⊢ φ \to ⋃ Z \neq \emptyset$
34		eluni2	$⊢ a \in ⋃ Z \leftrightarrow \exists i \in Z a \in i$
35		eluni2	$⊢ b \in ⋃ Z \leftrightarrow \exists j \in Z b \in j$
36	34 35	anbi12i	$⊢ (a \in ⋃ Z \land b \in ⋃ Z) \leftrightarrow (\exists i \in Z a \in i \land \exists j \in Z b \in j)$
37		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)$
38	3	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$
39	13	ad5antr	$⊢ (((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \to Z \subseteq LIdeal (R)$
40		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$
41	39 40	sseldd	$⊢ (((((φ \land x \in B) \land j \in Z) \land b \in j) \land i \in Z) \land a \in i) \to j \in LIdeal (R)$
42	41	adantr	$⊢ ((((((φ \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		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$
44		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$
45		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$
46	44 45	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$
47		eqid	$⊢ \cdot_{R} = \cdot_{R}$
48	15 1 47	lidlmcl	$⊢ ((R \in Ring \land j \in LIdeal (R)) \land (x \in B \land a \in j)) \to x \cdot_{R} a \in j$
49	38 42 43 46 48	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 \in j$
50		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$
51		eqid	$⊢ +_{R} = +_{R}$
52	15 51	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$
53	38 42 49 50 52	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$
54	40	adantr	$⊢ ((((((φ \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$
55		elunii	$⊢ ((x \cdot_{R} a) +_{R} b \in j \land j \in Z) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
56	53 54 55	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$
57	3	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$
58	39	adantr	$⊢ ((((((φ \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)$
59		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$
60	59	adantr	$⊢ ((((((φ \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$
61	58 60	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)$
62		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$
63		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$
64	15 1 47	lidlmcl	$⊢ ((R \in Ring \land i \in LIdeal (R)) \land (x \in B \land a \in i)) \to x \cdot_{R} a \in i$
65	57 61 62 63 64	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 \in i$
66		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$
67		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$
68	66 67	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$
69	15 51	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$
70	57 61 65 68 69	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$
71		elunii	$⊢ ((x \cdot_{R} a) +_{R} b \in i \land i \in Z) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
72	70 60 71	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$
73	8	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$
74		sorpssi	$⊢ ([\subset] Or Z \land (i \in Z \land j \in Z)) \to (i \subseteq j \lor j \subseteq i)$
75	73 59 40 74	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)$
76	56 72 75	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$
77	76	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$
78	77	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$
79	37 78	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$
80	79	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$
81	80	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$
82	36 81	sylan2b	$⊢ ((φ \land x \in B) \land (a \in ⋃ Z \land b \in ⋃ Z)) \to (x \cdot_{R} a) +_{R} b \in ⋃ Z$
83	82	ralrimivva	$⊢ (φ \land x \in B) \to \forall a \in ⋃ Z \forall b \in ⋃ Z (x \cdot_{R} a) +_{R} b \in ⋃ Z$
84	83	ralrimiva	$⊢ φ \to \forall x \in B \forall a \in ⋃ Z \forall b \in ⋃ Z (x \cdot_{R} a) +_{R} b \in ⋃ Z$
85	15 1 51 47	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)$
86	20 33 84 85	syl3anbrc	$⊢ φ \to ⋃ Z \in LIdeal (R)$
87	6	sselda	$⊢ (φ \land j \in Z) \to j \in P$
88		neeq1	$⊢ p = j \to (p \neq B \leftrightarrow j \neq B)$
89		sseq2	$⊢ p = j \to (I \subseteq p \leftrightarrow I \subseteq j)$
90	88 89	anbi12d	$⊢ p = j \to ((p \neq B \land I \subseteq p) \leftrightarrow (j \neq B \land I \subseteq j))$
91	90 2	elrab2	$⊢ j \in P \leftrightarrow (j \in LIdeal (R) \land (j \neq B \land I \subseteq j))$
92	87 91	sylib	$⊢ (φ \land j \in Z) \to (j \in LIdeal (R) \land (j \neq B \land I \subseteq j))$
93	92	simprld	$⊢ (φ \land j \in Z) \to j \neq B$
94		eqid	$⊢ 1_{R} = 1_{R}$
95	1 94	pridln1	$⊢ (R \in Ring \land j \in LIdeal (R) \land j \neq B) \to \neg 1_{R} \in j$
96	21 14 93 95	syl3anc	$⊢ (φ \land j \in Z) \to \neg 1_{R} \in j$
97	96	nrexdv	$⊢ φ \to \neg \exists j \in Z 1_{R} \in j$
98		eluni2	$⊢ 1_{R} \in ⋃ Z \leftrightarrow \exists j \in Z 1_{R} \in j$
99	97 98	sylnibr	$⊢ φ \to \neg 1_{R} \in ⋃ Z$
100	15 1 94	lidl1el	$⊢ (R \in Ring \land ⋃ Z \in LIdeal (R)) \to (1_{R} \in ⋃ Z \leftrightarrow ⋃ Z = B)$
101	3 86 100	syl2anc	$⊢ φ \to (1_{R} \in ⋃ Z \leftrightarrow ⋃ Z = B)$
102	101	necon3bbid	$⊢ φ \to (\neg 1_{R} \in ⋃ Z \leftrightarrow ⋃ Z \neq B)$
103	99 102	mpbid	$⊢ φ \to ⋃ Z \neq B$
104	92	simprrd	$⊢ (φ \land j \in Z) \to I \subseteq j$
105	104	ralrimiva	$⊢ φ \to \forall j \in Z I \subseteq j$
106		ssint	$⊢ I \subseteq ⋂ Z \leftrightarrow \forall j \in Z I \subseteq j$
107	105 106	sylibr	$⊢ φ \to I \subseteq ⋂ Z$
108		intssuni	$⊢ Z \neq \emptyset \to ⋂ Z \subseteq ⋃ Z$
109	7 108	syl	$⊢ φ \to ⋂ Z \subseteq ⋃ Z$
110	107 109	sstrd	$⊢ φ \to I \subseteq ⋃ Z$
111	103 110	jca	$⊢ φ \to (⋃ Z \neq B \land I \subseteq ⋃ Z)$
112	11 86 111	elrabd	$⊢ φ \to ⋃ Z \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\}$
113	112 2	eleqtrrdi	$⊢ φ \to ⋃ Z \in P$

Metamath Proof Explorer

Theorem ssmxidllem

Proof