Theorem mgmidsssn0

Description: Property of the set of identities of G . Either G has no identities, and O = (/) , or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypotheses	mgmidsssn0.b	$$⊢B={\mathrm{Base}}_G$$
	mgmidsssn0.z	$$⊢\underset{\dot{}}{0}=0_G$$
	mgmidsssn0.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	mgmidsssn0.o	$$⊢O=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
Assertion	mgmidsssn0	$$⊢G\in V\to O\subseteq \left\{\underset{\dot{}}{0}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		mgmidsssn0.b	$$⊢B={\mathrm{Base}}_G$$
2		mgmidsssn0.z	$$⊢\underset{\dot{}}{0}=0_G$$
3		mgmidsssn0.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		mgmidsssn0.o	$$⊢O=\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}$$
5		simpr	$$⊢\left(G\in V\wedge \left(x\in B\wedge \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)\right)\to \left(x\in B\wedge \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)$$
6		oveq1	$$⊢z=x\to z\underset{\dot{}}{+}y=x\underset{\dot{}}{+}y$$
7	6	eqeq1d	$$⊢z=x\to \left(z\underset{\dot{}}{+}y=y\leftrightarrow x\underset{\dot{}}{+}y=y\right)$$
8	7	ovanraleqv	$$⊢z=x\to \left(\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)\leftrightarrow \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)$$
9	8	rspcev	$$⊢\left(x\in B\wedge \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)\to \exists z\in B\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)$$
10	9	adantl	$$⊢\left(G\in V\wedge \left(x\in B\wedge \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)\right)\to \exists z\in B\forall y\in B\left(z\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}z=y\right)$$
11	1 2 3 10	ismgmid	$$⊢\left(G\in V\wedge \left(x\in B\wedge \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)\right)\to \left(\left(x\in B\wedge \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)\leftrightarrow \underset{\dot{}}{0}=x\right)$$
12	5 11	mpbid	$$⊢\left(G\in V\wedge \left(x\in B\wedge \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)\right)\to \underset{\dot{}}{0}=x$$
13	12	eqcomd	$$⊢\left(G\in V\wedge \left(x\in B\wedge \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)\right)\to x=\underset{\dot{}}{0}$$
14		velsn	$$⊢x\in \left\{\underset{\dot{}}{0}\right\}\leftrightarrow x=\underset{\dot{}}{0}$$
15	13 14	sylibr	$$⊢\left(G\in V\wedge \left(x\in B\wedge \forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right)\right)\to x\in \left\{\underset{\dot{}}{0}\right\}$$
16	15	expr	$$⊢\left(G\in V\wedge x\in B\right)\to \left(\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\to x\in \left\{\underset{\dot{}}{0}\right\}\right)$$
17	16	ralrimiva	$$⊢G\in V\to \forall x\in B\left(\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\to x\in \left\{\underset{\dot{}}{0}\right\}\right)$$
18		rabss	$$⊢\left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\subseteq \left\{\underset{\dot{}}{0}\right\}\leftrightarrow \forall x\in B\left(\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\to x\in \left\{\underset{\dot{}}{0}\right\}\right)$$
19	17 18	sylibr	$$⊢G\in V\to \left\{x\in B|\forall y\in B\left(x\underset{\dot{}}{+}y=y\wedge y\underset{\dot{}}{+}x=y\right)\right\}\subseteq \left\{\underset{\dot{}}{0}\right\}$$
20	4 19	eqsstrid	$$⊢G\in V\to O\subseteq \left\{\underset{\dot{}}{0}\right\}$$