This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-mxidl

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) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Assertion df-mxidl ⊢ MaxIdeal = r ∈ Ring ⟼ i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmxidl class MaxIdeal
1 vr setvar r
2 crg class Ring
3 vi setvar i
4 clidl class LIdeal
5 1 cv setvar r
6 5 4 cfv class LIdeal ⁡ r
7 3 cv setvar i
8 cbs class Base
9 5 8 cfv class Base r
10 7 9 wne wff i ≠ Base r
11 vj setvar j
12 11 cv setvar j
13 7 12 wss wff i ⊆ j
14 12 7 wceq wff j = i
15 12 9 wceq wff j = Base r
16 14 15 wo wff j = i ∨ j = Base r
17 13 16 wi wff i ⊆ j → j = i ∨ j = Base r
18 17 11 6 wral wff ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r
19 10 18 wa wff i ≠ Base r ∧ ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r
20 19 3 6 crab class i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r
21 1 2 20 cmpt class r ∈ Ring ⟼ i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r
22 0 21 wceq wff MaxIdeal = r ∈ Ring ⟼ i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r