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	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{Mgm}$$

Proof

Step	Hyp	Ref	Expression
1		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{V}$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}$$
4	3	grpbase	$$⊢\varnothing \in \mathrm{V}\to \varnothing ={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}$$
5	4	eqcomd	$$⊢\varnothing \in \mathrm{V}\to {\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}=\varnothing$$
6	2 5	ax-mp	$$⊢{\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}=\varnothing$$
7		mgm0	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{V}\wedge {\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}=\varnothing \right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{Mgm}$$
8	1 6 7	mp2an	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{Mgm}$$