ismgmd

Description: Deduce a magma from its properties. (Contributed by AV, 25-Feb-2020)

	Ref	Expression
Hypotheses	ismgmd.b	$⊢ φ \to B = {Base}_{G}$
	ismgmd.0	$⊢ φ \to G \in V$
	ismgmd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
	ismgmd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
Assertion	ismgmd	$⊢ φ \to G \in Mgm$

Step	Hyp	Ref	Expression
1		ismgmd.b	$⊢ φ \to B = {Base}_{G}$
2		ismgmd.0	$⊢ φ \to G \in V$
3		ismgmd.p	$⊢ φ \to \underset{˙}{+} = +_{G}$
4		ismgmd.c	$⊢ (φ \land x \in B \land y \in B) \to x \underset{˙}{+} y \in B$
5	4	3expb	$⊢ (φ \land (x \in B \land y \in B)) \to x \underset{˙}{+} y \in B$
6	5	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B x \underset{˙}{+} y \in B$
7	3	oveqd	$⊢ φ \to x \underset{˙}{+} y = x +_{G} y$
8	7 1	eleq12d	$⊢ φ \to (x \underset{˙}{+} y \in B \leftrightarrow x +_{G} y \in {Base}_{G})$
9	1 8	raleqbidv	$⊢ φ \to (\forall y \in B x \underset{˙}{+} y \in B \leftrightarrow \forall y \in {Base}_{G} x +_{G} y \in {Base}_{G})$
10	1 9	raleqbidv	$⊢ φ \to (\forall x \in B \forall y \in B x \underset{˙}{+} y \in B \leftrightarrow \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y \in {Base}_{G})$
11	6 10	mpbid	$⊢ φ \to \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y \in {Base}_{G}$
12		eqid	$⊢ {Base}_{G} = {Base}_{G}$
13		eqid	$⊢ +_{G} = +_{G}$
14	12 13	ismgm	$⊢ G \in V \to (G \in Mgm \leftrightarrow \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y \in {Base}_{G})$
15	2 14	syl	$⊢ φ \to (G \in Mgm \leftrightarrow \forall x \in {Base}_{G} \forall y \in {Base}_{G} x +_{G} y \in {Base}_{G})$
16	11 15	mpbird	$⊢ φ \to G \in Mgm$

Metamath Proof Explorer