Metamath Proof Explorer

Theorem mxidlval

Description: The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by Thierry Arnoux, 19-Jan-2024)

Ref Expression
Hypothesis mxidlval.1 ⊢ B = Base R
Assertion mxidlval ⊢ R ∈ Ring → MaxIdeal ⁡ R = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B

Proof

Step Hyp Ref Expression
1 mxidlval.1 ⊢ B = Base R
2 fveq2 ⊢ r = R → LIdeal ⁡ r = LIdeal ⁡ R
3 fveq2 ⊢ r = R → Base r = Base R
4 3 1 eqtr4di ⊢ r = R → Base r = B
5 4 neeq2d ⊢ r = R → i ≠ Base r ↔ i ≠ B
6 4 eqeq2d ⊢ r = R → j = Base r ↔ j = B
7 6 orbi2d ⊢ r = R → j = i ∨ j = Base r ↔ j = i ∨ j = B
8 7 imbi2d ⊢ r = R → i ⊆ j → j = i ∨ j = Base r ↔ i ⊆ j → j = i ∨ j = B
9 2 8 raleqbidv ⊢ r = R → ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r ↔ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B
10 5 9 anbi12d ⊢ r = R → i ≠ Base r ∧ ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r ↔ i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B
11 2 10 rabeqbidv ⊢ r = R → i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B
12 df-mxidl ⊢ MaxIdeal = r ∈ Ring ⟼ i ∈ LIdeal ⁡ r | i ≠ Base r ∧ ∀ j ∈ LIdeal ⁡ r i ⊆ j → j = i ∨ j = Base r
13 fvex ⊢ LIdeal ⁡ R ∈ V
14 13 rabex ⊢ i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B ∈ V
15 11 12 14 fvmpt ⊢ R ∈ Ring → MaxIdeal ⁡ R = i ∈ LIdeal ⁡ R | i ≠ B ∧ ∀ j ∈ LIdeal ⁡ R i ⊆ j → j = i ∨ j = B