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