Theorem sgrp0b

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

	Ref	Expression
Assertion	sgrp0b	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{Smgrp}$$

Proof

Step	Hyp	Ref	Expression
1		mgm0b	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{Mgm}$$
2		ral0	$$⊢\forall x\in \varnothing \forall y\in \varnothing \forall z\in \varnothing \left(x{+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}y\right){+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}z=x{+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}\left(y{+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}z\right)$$
3		0ex	$$⊢\varnothing \in \mathrm{V}$$
4		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}$$
5	4	grpbase	$$⊢\varnothing \in \mathrm{V}\to \varnothing ={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}$$
6	3 5	ax-mp	$$⊢\varnothing ={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}$$
7		eqid	$$⊢{+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}$$
8	6 7	issgrp	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{Smgrp}\leftrightarrow \left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{Mgm}\wedge \forall x\in \varnothing \forall y\in \varnothing \forall z\in \varnothing \left(x{+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}y\right){+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}z=x{+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}\left(y{+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}}z\right)\right)$$
9	1 2 8	mpbir2an	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},\varnothing ⟩,⟨{+}_{\mathrm{ndx}},O⟩\right\}\in \mathrm{Smgrp}$$