ssmxidl

Description: Let R be a ring, and let I be a proper ideal of R . Then there is a maximal ideal of R containing I . (Contributed by Thierry Arnoux, 10-Apr-2024)

		Ref	Expression
	Hypothesis	ssmxidl.1	$⊢ B = {Base}_{R}$
	Assertion	ssmxidl	Could not format assertion : No typesetting found for \|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		ssmxidl.1	$⊢ B = {Base}_{R}$
2		neeq1	$⊢ p = I \to (p \neq B \leftrightarrow I \neq B)$
3		sseq2	$⊢ p = I \to (I \subseteq p \leftrightarrow I \subseteq I)$
4	2 3	anbi12d	$⊢ p = I \to ((p \neq B \land I \subseteq p) \leftrightarrow (I \neq B \land I \subseteq I))$
5		simp2	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to I \in LIdeal (R)$
6		simp3	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to I \neq B$
7		ssidd	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to I \subseteq I$
8	6 7	jca	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to (I \neq B \land I \subseteq I)$
9	4 5 8	elrabd	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to I \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\}$
10	9	ne0d	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neq \emptyset$
11		eqid	$⊢ \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} = \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\}$
12		simpl1	$⊢ ((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z)) \to R \in Ring$
13		simpl2	$⊢ ((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z)) \to I \in LIdeal (R)$
14		simpl3	$⊢ ((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z)) \to I \neq B$
15		simpr1	$⊢ ((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z)) \to z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\}$
16		simpr2	$⊢ ((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z)) \to z \neq \emptyset$
17		simpr3	$⊢ ((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z)) \to [\subset] Or z$
18	1 11 12 13 14 15 16 17	ssmxidllem	$⊢ ((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z)) \to ⋃ z \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\}$
19	18	ex	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to ((z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\})$
20	19	alrimiv	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to \forall z ((z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\})$
21		fvex	$⊢ LIdeal (R) \in V$
22	21	rabex	$⊢ \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \in V$
23	22	zornn0	$⊢ (\{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neq \emptyset \land \forall z ((z \subseteq \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \land z \neq \emptyset \land [\subset] Or z) \to ⋃ z \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\})) \to \exists m \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j$
24	10 20 23	syl2anc	$⊢ (R \in Ring \land I \in LIdeal (R) \land I \neq B) \to \exists m \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j$
25		neeq1	$⊢ p = m \to (p \neq B \leftrightarrow m \neq B)$
26		sseq2	$⊢ p = m \to (I \subseteq p \leftrightarrow I \subseteq m)$
27	25 26	anbi12d	$⊢ p = m \to ((p \neq B \land I \subseteq p) \leftrightarrow (m \neq B \land I \subseteq m))$
28	27	elrab	$⊢ m \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \leftrightarrow (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))$
29	28	anbi2i	$⊢ ((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land m \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\}) \leftrightarrow ((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m)))$
30		simpll1	$⊢ (((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \to R \in Ring$
31		simplrl	$⊢ (((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \to m \in LIdeal (R)$
32		simplr	$⊢ (((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \to (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))$
33	32	simprld	$⊢ (((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \to m \neq B$
34		psseq2	$⊢ j = k \to (m \subset j \leftrightarrow m \subset k)$
35	34	notbid	$⊢ j = k \to (\neg m \subset j \leftrightarrow \neg m \subset k)$
36		simp-4r	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j$
37		neeq1	$⊢ p = k \to (p \neq B \leftrightarrow k \neq B)$
38		sseq2	$⊢ p = k \to (I \subseteq p \leftrightarrow I \subseteq k)$
39	37 38	anbi12d	$⊢ p = k \to ((p \neq B \land I \subseteq p) \leftrightarrow (k \neq B \land I \subseteq k))$
40		simpllr	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to k \in LIdeal (R)$
41		simpr	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to \neg k = B$
42	41	neqned	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to k \neq B$
43		simp-5r	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))$
44	43	simprrd	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to I \subseteq m$
45		simplr	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to m \subseteq k$
46	44 45	sstrd	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to I \subseteq k$
47	42 46	jca	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to (k \neq B \land I \subseteq k)$
48	39 40 47	elrabd	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to k \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\}$
49	35 36 48	rspcdva	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to \neg m \subset k$
50		npss	$⊢ \neg m \subset k \leftrightarrow (m \subseteq k \to m = k)$
51	50	biimpi	$⊢ \neg m \subset k \to (m \subseteq k \to m = k)$
52	49 45 51	sylc	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to m = k$
53	52	equcomd	$⊢ ((((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \land \neg k = B) \to k = m$
54	53	ex	$⊢ (((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \to (\neg k = B \to k = m)$
55	54	orrd	$⊢ (((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \to (k = B \lor k = m)$
56	55	orcomd	$⊢ (((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \land m \subseteq k) \to (k = m \lor k = B)$
57	56	ex	$⊢ ((((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \land k \in LIdeal (R)) \to (m \subseteq k \to (k = m \lor k = B))$
58	57	ralrimiva	$⊢ (((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \to \forall k \in LIdeal (R) (m \subseteq k \to (k = m \lor k = B))$
59	1	ismxidl	Could not format ( R e. Ring -> ( m e. ( MaxIdeal ` R ) <-> ( m e. ( LIdeal ` R ) /\ m =/= B /\ A. k e. ( LIdeal ` R ) ( m C_ k -> ( k = m \/ k = B ) ) ) ) ) : No typesetting found for \|- ( R e. Ring -> ( m e. ( MaxIdeal ` R ) <-> ( m e. ( LIdeal ` R ) /\ m =/= B /\ A. k e. ( LIdeal ` R ) ( m C_ k -> ( k = m \/ k = B ) ) ) ) ) with typecode \|-
60	59	biimpar	Could not format ( ( R e. Ring /\ ( m e. ( LIdeal ` R ) /\ m =/= B /\ A. k e. ( LIdeal ` R ) ( m C_ k -> ( k = m \/ k = B ) ) ) ) -> m e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ( R e. Ring /\ ( m e. ( LIdeal ` R ) /\ m =/= B /\ A. k e. ( LIdeal ` R ) ( m C_ k -> ( k = m \/ k = B ) ) ) ) -> m e. ( MaxIdeal ` R ) ) with typecode \|-
61	30 31 33 58 60	syl13anc	Could not format ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j ) -> m e. ( MaxIdeal ` R ) ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j ) -> m e. ( MaxIdeal ` R ) ) with typecode \|-
62	32	simprrd	$⊢ (((R \in Ring \land I \in LIdeal (R) \land I \neq B) \land (m \in LIdeal (R) \land (m \neq B \land I \subseteq m))) \land \forall j \in \{p \in LIdeal (R) \| (p \neq B \land I \subseteq p)\} \neg m \subset j) \to I \subseteq m$
63	61 62	jca	Could not format ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( MaxIdeal ` R ) /\ I C_ m ) ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ ( m e. ( LIdeal ` R ) /\ ( m =/= B /\ I C_ m ) ) ) /\ A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( MaxIdeal ` R ) /\ I C_ m ) ) with typecode \|-
64	29 63	sylanb	Could not format ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ m e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } ) /\ A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( MaxIdeal ` R ) /\ I C_ m ) ) : No typesetting found for \|- ( ( ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) /\ m e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } ) /\ A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( MaxIdeal ` R ) /\ I C_ m ) ) with typecode \|-
65	64	expl	Could not format ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> ( ( m e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } /\ A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( MaxIdeal ` R ) /\ I C_ m ) ) ) : No typesetting found for \|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> ( ( m e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } /\ A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j ) -> ( m e. ( MaxIdeal ` R ) /\ I C_ m ) ) ) with typecode \|-
66	65	reximdv2	Could not format ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> ( E. m e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j -> E. m e. ( MaxIdeal ` R ) I C_ m ) ) : No typesetting found for \|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> ( E. m e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } A. j e. { p e. ( LIdeal ` R ) \| ( p =/= B /\ I C_ p ) } -. m C. j -> E. m e. ( MaxIdeal ` R ) I C_ m ) ) with typecode \|-
67	24 66	mpd	Could not format ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) : No typesetting found for \|- ( ( R e. Ring /\ I e. ( LIdeal ` R ) /\ I =/= B ) -> E. m e. ( MaxIdeal ` R ) I C_ m ) with typecode \|-

Metamath Proof Explorer

Theorem ssmxidl

Proof