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 ≠ ∅