Theorem ismgmd

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

	Ref	Expression
Hypotheses	ismgmd.b	$$⊢\phi \to B={\mathrm{Base}}_G$$
	ismgmd.0	$$⊢\phi \to G\in V$$
	ismgmd.p	$$⊢\phi \to \underset{\dot{}}{+}={+}_G$$
	ismgmd.c	$$⊢\left(\phi \wedge x\in B\wedge y\in B\right)\to x\underset{\dot{}}{+}y\in B$$
Assertion	ismgmd	$$⊢\phi \to G\in \mathrm{Mgm}$$

Proof

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