Metamath Proof Explorer

Definition 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 ∈ RingOps ⟼ i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ j ∈ Idl ⁡ r i ⊆ j → j = i ∨ 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 ≠ ran ⁡ 1 st ⁡ r
12 vj setvar j
13 12 cv setvar j
14 7 13 wss wff i ⊆ 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 ∨ j = ran ⁡ 1 st ⁡ r
18 14 17 wi wff i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r
19 18 12 6 wral wff ∀ j ∈ Idl ⁡ r i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r
20 11 19 wa wff i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ j ∈ Idl ⁡ r i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r
21 20 3 6 crab class i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ j ∈ Idl ⁡ r i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r
22 1 2 21 cmpt class r ∈ RingOps ⟼ i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ j ∈ Idl ⁡ r i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r
23 0 22 wceq wff MaxIdl = r ∈ RingOps ⟼ i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ j ∈ Idl ⁡ r i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r