Metamath Proof Explorer

Theorem maxidlnr

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

Ref Expression
Hypotheses maxidlnr.1 ⊢ G = 1 st ⁡ R
maxidlnr.2 ⊢ X = ran ⁡ G
Assertion maxidlnr ⊢ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R → M ≠ 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 simp2d ⊢ R ∈ RingOps ∧ M ∈ MaxIdl ⁡ R → M ≠ X