Metamath Proof Explorer

Theorem ismaxidl

Description: The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011)

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

Proof

Step Hyp Ref Expression
1 ismaxidl.1 ⊢ G = 1 st ⁡ R
2 ismaxidl.2 ⊢ X = ran ⁡ G
3 1 2 maxidlval ⊢ R ∈ RingOps → MaxIdl ⁡ R = i ∈ Idl ⁡ R | i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X
4 3 eleq2d ⊢ R ∈ RingOps → M ∈ MaxIdl ⁡ R ↔ M ∈ i ∈ Idl ⁡ R | i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X
5 neeq1 ⊢ i = M → i ≠ X ↔ M ≠ X
6 sseq1 ⊢ i = M → i ⊆ j ↔ M ⊆ j
7 eqeq2 ⊢ i = M → j = i ↔ j = M
8 7 orbi1d ⊢ i = M → j = i ∨ j = X ↔ j = M ∨ j = X
9 6 8 imbi12d ⊢ i = M → i ⊆ j → j = i ∨ j = X ↔ M ⊆ j → j = M ∨ j = X
10 9 ralbidv ⊢ i = M → ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X ↔ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X
11 5 10 anbi12d ⊢ i = M → i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X ↔ M ≠ X ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X
12 11 elrab ⊢ M ∈ i ∈ Idl ⁡ R | i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X ↔ M ∈ Idl ⁡ R ∧ M ≠ X ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X
13 3anass ⊢ M ∈ Idl ⁡ R ∧ M ≠ X ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X ↔ M ∈ Idl ⁡ R ∧ M ≠ X ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X
14 12 13 bitr4i ⊢ M ∈ i ∈ Idl ⁡ R | i ≠ X ∧ ∀ j ∈ Idl ⁡ R i ⊆ j → j = i ∨ j = X ↔ M ∈ Idl ⁡ R ∧ M ≠ X ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X
15 4 14 bitrdi ⊢ R ∈ RingOps → M ∈ MaxIdl ⁡ R ↔ M ∈ Idl ⁡ R ∧ M ≠ X ∧ ∀ j ∈ Idl ⁡ R M ⊆ j → j = M ∨ j = X