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 = ( Base ` G )
	mgmidsssn0.z	|- .0. = ( 0g ` G )
	mgmidsssn0.p	|- .+ = ( +g ` G )
	mgmidsssn0.o	|- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
Assertion	mgmidsssn0	|- ( G e. V -> O C_ { .0. } )

Proof

Step	Hyp	Ref	Expression
1		mgmidsssn0.b	|- B = ( Base ` G )
2		mgmidsssn0.z	|- .0. = ( 0g ` G )
3		mgmidsssn0.p	|- .+ = ( +g ` G )
4		mgmidsssn0.o	|- O = { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) }
5		simpr	|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
6		oveq1	|- ( z = x -> ( z .+ y ) = ( x .+ y ) )
7	6	eqeq1d	|- ( z = x -> ( ( z .+ y ) = y <-> ( x .+ y ) = y ) )
8	7	ovanraleqv	|- ( z = x -> ( A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) <-> A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) )
9	8	rspcev	|- ( ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) -> E. z e. B A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) )
10	9	adantl	|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> E. z e. B A. y e. B ( ( z .+ y ) = y /\ ( y .+ z ) = y ) )
11	1 2 3 10	ismgmid	|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> ( ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) <-> .0. = x ) )
12	5 11	mpbid	|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> .0. = x )
13	12	eqcomd	|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> x = .0. )
14		velsn	|- ( x e. { .0. } <-> x = .0. )
15	13 14	sylibr	|- ( ( G e. V /\ ( x e. B /\ A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) ) ) -> x e. { .0. } )
16	15	expr	|- ( ( G e. V /\ x e. B ) -> ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> x e. { .0. } ) )
17	16	ralrimiva	|- ( G e. V -> A. x e. B ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> x e. { .0. } ) )
18		rabss	|- ( { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { .0. } <-> A. x e. B ( A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) -> x e. { .0. } ) )
19	17 18	sylibr	|- ( G e. V -> { x e. B | A. y e. B ( ( x .+ y ) = y /\ ( y .+ x ) = y ) } C_ { .0. } )
20	4 19	eqsstrid	|- ( G e. V -> O C_ { .0. } )