Theorem abln0

Description: Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019)

	Ref	Expression
Assertion	abln0	⊢ Abel ≠ ∅

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑖 ∈ V
2		eqid	⊢ { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } = { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ }
3	2	abl1	⊢ ( 𝑖 ∈ V → { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ∈ Abel )
4		ne0i	⊢ ( { ⟨ ( Base ‘ ndx ) , { 𝑖 } ⟩ , ⟨ ( +g ‘ ndx ) , { ⟨ ⟨ 𝑖 , 𝑖 ⟩ , 𝑖 ⟩ } ⟩ } ∈ Abel → Abel ≠ ∅ )
5	1 3 4	mp2b	⊢ Abel ≠ ∅