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	$$⊢\left(M\in V\wedge {\mathrm{Base}}_M=\varnothing \right)\to M\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		rzal	$$⊢{\mathrm{Base}}_M=\varnothing \to \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_{M}x{+}_{M}y\in {\mathrm{Base}}_M$$
2	1	adantl	$$⊢\left(M\in V\wedge {\mathrm{Base}}_M=\varnothing \right)\to \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_{M}x{+}_{M}y\in {\mathrm{Base}}_M$$
3		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
4		eqid	$$⊢{+}_M={+}_M$$
5	3 4	ismgm	$$⊢M\in V\to \left(M\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_{M}x{+}_{M}y\in {\mathrm{Base}}_M\right)$$
6	5	adantr	$$⊢\left(M\in V\wedge {\mathrm{Base}}_M=\varnothing \right)\to \left(M\in \mathrm{Mgm}\leftrightarrow \forall x\in {\mathrm{Base}}_M\forall y\in {\mathrm{Base}}_{M}x{+}_{M}y\in {\mathrm{Base}}_M\right)$$
7	2 6	mpbird	$$⊢\left(M\in V\wedge {\mathrm{Base}}_M=\varnothing \right)\to M\in \mathrm{Mgm}$$