Metamath Proof Explorer

Theorem maxidlval

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

Ref Expression
Hypotheses maxidlval.1 ⊢ G = 1 st ⁡ R
maxidlval.2 ⊢ X = ran ⁡ G
Assertion maxidlval ⊢ R ∈ RingOps → MaxIdl ⁡ R = i ∈ Idl ⁡ R | i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X

Proof

Step Hyp Ref Expression
1 maxidlval.1 ⊢ G = 1 st ⁡ R
2 maxidlval.2 ⊢ X = ran ⁡ G
3 fveq2 ⊢ r = R → Idl ⁡ r = Idl ⁡ R
4 fveq2 ⊢ r = R → 1 st ⁡ r = 1 st ⁡ R
5 4 1 eqtr4di ⊢ r = R → 1 st ⁡ r = G
6 5 rneqd ⊢ r = R → ran ⁡ 1 st ⁡ r = ran ⁡ G
7 6 2 eqtr4di ⊢ r = R → ran ⁡ 1 st ⁡ r = X
8 7 neeq2d ⊢ r = R → i ≠ ran ⁡ 1 st ⁡ r ↔ i ≠ X
9 7 eqeq2d ⊢ r = R → j = ran ⁡ 1 st ⁡ r ↔ j = X
10 9 orbi2d ⊢ r = R → j = i ∨ j = ran ⁡ 1 st ⁡ r ↔ j = i ∨ j = X
11 10 imbi2d ⊢ r = R → i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r ↔ i ⊆ j → j = i ∨ j = X
12 3 11 raleqbidv ⊢ r = R → ∀ j ∈ Idl ⁡ r i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r ↔ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X
13 8 12 anbi12d ⊢ r = R → i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ j ∈ Idl ⁡ r i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r ↔ i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X
14 3 13 rabeqbidv ⊢ r = R → i ∈ Idl ⁡ r | i ≠ ran ⁡ 1 st ⁡ r ∧ ∀ j ∈ Idl ⁡ r i ⊆ j → j = i ∨ j = ran ⁡ 1 st ⁡ r = i ∈ Idl ⁡ R | i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X
15 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
16 fvex ⊢ Idl ⁡ R ∈ V
17 16 rabex ⊢ i ∈ Idl ⁡ R | i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X ∈ V
18 14 15 17 fvmpt ⊢ R ∈ RingOps → MaxIdl ⁡ R = i ∈ Idl ⁡ R | i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X