Metamath Proof Explorer

Theorem pridlnr

Description: A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses pridlnr.1 ⊢ G = 1 st ⁡ R
prdilnr.2 ⊢ X = ran ⁡ G
Assertion pridlnr ⊢ R ∈ RingOps ∧ P ∈ PrIdl ⁡ R → P ≠ X

Proof

Step Hyp Ref Expression
1 pridlnr.1 ⊢ G = 1 st ⁡ R
2 prdilnr.2 ⊢ X = ran ⁡ G
3 eqid ⊢ 2 nd ⁡ R = 2 nd ⁡ R
4 1 3 2 ispridl ⊢ R ∈ RingOps → P ∈ PrIdl ⁡ R ↔ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ R y ∈ P → a ⊆ P ∨ b ⊆ P
5 3anan12 ⊢ P ∈ Idl ⁡ R ∧ P ≠ X ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ R y ∈ P → a ⊆ P ∨ b ⊆ P ↔ P ≠ X ∧ P ∈ Idl ⁡ R ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ R y ∈ P → a ⊆ P ∨ b ⊆ P
6 4 5 bitrdi ⊢ R ∈ RingOps → P ∈ PrIdl ⁡ R ↔ P ≠ X ∧ P ∈ Idl ⁡ R ∧ ∀ a ∈ Idl ⁡ R ∀ b ∈ Idl ⁡ R ∀ x ∈ a ∀ y ∈ b x 2 nd ⁡ R y ∈ P → a ⊆ P ∨ b ⊆ P
7 6 simprbda ⊢ R ∈ RingOps ∧ P ∈ PrIdl ⁡ R → P ≠ X