This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mgm0b

Description: The structure with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021)

Ref Expression
Assertion mgm0b { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ∈ Mgm

Proof

Step Hyp Ref Expression
1 prex ⊢ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ∈ V
2 0ex ⊢ ∅ ∈ V
3 eqid ⊢ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } = { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ }
4 3 grpbase ⊢ ( ∅ ∈ V → ∅ = ( Base ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) )
5 4 eqcomd ⊢ ( ∅ ∈ V → ( Base ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) = ∅ )
6 2 5 ax-mp ⊢ ( Base ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) = ∅
7 mgm0 ⊢ ( ( { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ∈ V ∧ ( Base ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) = ∅ ) → { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ∈ Mgm )
8 1 6 7 mp2an ⊢ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ∈ Mgm