Metamath Proof Explorer

Theorem maxidlmax

Description: A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses maxidlnr.1 ⊢ G = 1 st ⁡ R
maxidlnr.2 ⊢ X = ran ⁡ G
Assertion maxidlmax ⊢ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R ∧ I ∈ Idl ⁡ R ∧ M ⊆ I → I = M ∨ I = X

Proof

Step Hyp Ref Expression
1 maxidlnr.1 ⊢ G = 1 st ⁡ R
2 maxidlnr.2 ⊢ X = ran ⁡ G
3 1 2 ismaxidl ⊢ R ∈ RingOps → M ∈ MaxIdl ⁡ R ↔ M ∈ Idl ⁡ R ∧ M ≠ X ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X
4 3 biimpa ⊢ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R → M ∈ Idl ⁡ R ∧ M ≠ X ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X
5 4 simp3d ⊢ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R → ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X
6 sseq2 ⊢ j = I → M ⊆ j ↔ M ⊆ I
7 eqeq1 ⊢ j = I → j = M ↔ I = M
8 eqeq1 ⊢ j = I → j = X ↔ I = X
9 7 8 orbi12d ⊢ j = I → j = M ∨ j = X ↔ I = M ∨ I = X
10 6 9 imbi12d ⊢ j = I → M ⊆ j → j = M ∨ j = X ↔ M ⊆ I → I = M ∨ I = X
11 10 rspcva ⊢ I ∈ Idl ⁡ R ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X → M ⊆ I → I = M ∨ I = X
12 5 11 sylan2 ⊢ I ∈ Idl ⁡ R ∧ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R → M ⊆ I → I = M ∨ I = X
13 12 ancoms ⊢ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R ∧ I ∈ Idl ⁡ R → M ⊆ I → I = M ∨ I = X
14 13 impr ⊢ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R ∧ I ∈ Idl ⁡ R ∧ M ⊆ I → I = M ∨ I = X