Theorem mgmidcl

Description: The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014)

	Ref	Expression
Hypotheses	ismgmid.b	$$⊢B={\mathrm{Base}}_G$$
	ismgmid.o	$$⊢\underset{\dot{}}{0}=0_G$$
	ismgmid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mgmidcl.e	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
Assertion	mgmidcl	$$⊢\phi \to \underset{\dot{}}{0}\in B$$

Proof

Step	Hyp	Ref	Expression
1		ismgmid.b	$$⊢B={\mathrm{Base}}_G$$
2		ismgmid.o	$$⊢\underset{\dot{}}{0}=0_G$$
3		ismgmid.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		mgmidcl.e	$$⊢\phi \to \exists e\in B\forall x\in B\left(e\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}e=x\right)$$
5		eqid	$$⊢\underset{\dot{}}{0}=\underset{\dot{}}{0}$$
6	1 2 3 4	ismgmid	$$⊢\phi \to \left(\left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{0}\right)$$
7	5 6	mpbiri	$$⊢\phi \to \left(\underset{\dot{}}{0}\in B\wedge \forall x\in B\left(\underset{\dot{}}{0}\underset{\dot{}}{+}x=x\wedge x\underset{\dot{}}{+}\underset{\dot{}}{0}=x\right)\right)$$
8	7	simpld	$$⊢\phi \to \underset{\dot{}}{0}\in B$$