df-maxidl

Description: Define the class of maximal ideals of a ring R . A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011)

		Ref	Expression
	Assertion	df-maxidl	$⊢ MaxIdl = (r \in RingOps ⟼ \{i \in Idl (r) \| (i \neq ran 1^{st} (r) \land \forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r))))\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmaxidl	$class MaxIdl$
1		vr	$setvar r$
2		crngo	$class RingOps$
3		vi	$setvar i$
4		cidl	$class Idl$
5	1	cv	$setvar r$
6	5 4	cfv	$class Idl (r)$
7	3	cv	$setvar i$
8		c1st	$class 1^{st}$
9	5 8	cfv	$class 1^{st} (r)$
10	9	crn	$class ran 1^{st} (r)$
11	7 10	wne	$wff i \neq ran 1^{st} (r)$
12		vj	$setvar j$
13	12	cv	$setvar j$
14	7 13	wss	$wff i \subseteq j$
15	13 7	wceq	$wff j = i$
16	13 10	wceq	$wff j = ran 1^{st} (r)$
17	15 16	wo	$wff (j = i \lor j = ran 1^{st} (r))$
18	14 17	wi	$wff (i \subseteq j \to (j = i \lor j = ran 1^{st} (r)))$
19	18 12 6	wral	$wff \forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r)))$
20	11 19	wa	$wff (i \neq ran 1^{st} (r) \land \forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r))))$
21	20 3 6	crab	$class \{i \in Idl (r) \| (i \neq ran 1^{st} (r) \land \forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r))))\}$
22	1 2 21	cmpt	$class (r \in RingOps ⟼ \{i \in Idl (r) \| (i \neq ran 1^{st} (r) \land \forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r))))\})$
23	0 22	wceq	$wff MaxIdl = (r \in RingOps ⟼ \{i \in Idl (r) \| (i \neq ran 1^{st} (r) \land \forall j \in Idl (r) (i \subseteq j \to (j = i \lor j = ran 1^{st} (r))))\})$

Metamath Proof Explorer

Definition df-maxidl

Detailed syntax breakdown