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