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

Metamath Proof Explorer

Theorem sgrp0b

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

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

Proof

Step Hyp Ref Expression
1 mgm0b ⊢ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ∈ Mgm
2 ral0 ⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ( ( 𝑥 ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) 𝑦 ) ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) 𝑧 ) = ( 𝑥 ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) ( 𝑦 ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) 𝑧 ) )
3 0ex ⊢ ∅ ∈ V
4 eqid ⊢ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } = { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ }
5 4 grpbase ⊢ ( ∅ ∈ V → ∅ = ( Base ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) )
6 3 5 ax-mp ⊢ ∅ = ( Base ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } )
7 eqid ⊢ ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } )
8 6 7 issgrp ⊢ ( { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ∈ Smgrp ↔ ( { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ∈ Mgm ∧ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ( ( 𝑥 ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) 𝑦 ) ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) 𝑧 ) = ( 𝑥 ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) ( 𝑦 ( +g ‘ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ) 𝑧 ) ) ) )
9 1 2 8 mpbir2an ⊢ { ⟨ ( Base ‘ ndx ) , ∅ ⟩ , ⟨ ( +g ‘ ndx ) , 𝑂 ⟩ } ∈ Smgrp