Theorem mgm0

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

	Ref	Expression
Assertion	mgm0	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → 𝑀 ∈ Mgm )

Proof

Step	Hyp	Ref	Expression
1		rzal	⊢ ( ( Base ‘ 𝑀 ) = ∅ → ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
2	1	adantl	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) )
3		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
4		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
5	3 4	ismgm	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) )
6	5	adantr	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → ( 𝑀 ∈ Mgm ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑀 ) ∀ 𝑦 ∈ ( Base ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ∈ ( Base ‘ 𝑀 ) ) )
7	2 6	mpbird	⊢ ( ( 𝑀 ∈ 𝑉 ∧ ( Base ‘ 𝑀 ) = ∅ ) → 𝑀 ∈ Mgm )