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

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

Metamath Proof Explorer