Theorem 0mgm

Description: A set with an empty base set is always a magma. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypothesis	0mgm.b	⊢ ( Base ‘ 𝑀 ) = ∅
Assertion	0mgm	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ Mgm )

Proof

Step	Hyp	Ref	Expression
1		0mgm.b	⊢ ( Base ‘ 𝑀 ) = ∅
2		ral0	⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ∅
3	1	eqcomi	⊢ ∅ = ( Base ‘ 𝑀 )
4		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
5	3 4	ismgm	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ∅ ) )
6	2 5	mpbiri	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ Mgm )