Metamath Proof Explorer


Theorem ringn0

Description: Rings exist. (Contributed by AV, 29-Apr-2019)

Ref Expression
Assertion ringn0 Ring ≠ ∅

Proof

Step Hyp Ref Expression
1 vex 𝑧 ∈ V
2 eqid { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ }
3 2 ring1 ( 𝑧 ∈ V → { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ∈ Ring )
4 ne0i ( { ⟨ ( Base ‘ ndx ) , { 𝑧 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ , ⟨ ( .r ‘ ndx ) , { ⟨ ⟨ 𝑧 , 𝑧 ⟩ , 𝑧 ⟩ } ⟩ } ∈ Ring → Ring ≠ ∅ )
5 1 3 4 mp2b Ring ≠ ∅