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	Could not format assertion : No typesetting found for |- { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Smgrp with typecode |-

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	Could not format ( { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Smgrp <-> ( { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Mgm /\ A. x e. (/) A. y e. (/) A. z e. (/) ( ( x ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) y ) ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) z ) = ( x ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) ( y ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) z ) ) ) ) : No typesetting found for |- ( { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Smgrp <-> ( { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Mgm /\ A. x e. (/) A. y e. (/) A. z e. (/) ( ( x ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) y ) ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) z ) = ( x ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) ( y ( +g ` { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } ) z ) ) ) ) with typecode |-
9	1 2 8	mpbir2an	Could not format { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Smgrp : No typesetting found for |- { <. ( Base ` ndx ) , (/) >. , <. ( +g ` ndx ) , O >. } e. Smgrp with typecode |-