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	$⊢ \{⟨{Base}_{ndx}, \emptyset⟩, ⟨+_{ndx}, O⟩\} \in Smgrp$

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

Metamath Proof Explorer