Metamath Proof Explorer


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