Theorem grpoidval

Description: Lemma for grpoidcl and others. (Contributed by NM, 5-Feb-2010) (Proof shortened by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpoidval.1	|- X = ran G
	grpoidval.2	|- U = ( GId ` G )
Assertion	grpoidval	|- ( G e. GrpOp -> U = ( iota_ u e. X A. x e. X ( u G x ) = x ) )

Proof

Step	Hyp	Ref	Expression
1		grpoidval.1	|- X = ran G
2		grpoidval.2	|- U = ( GId ` G )
3	1	gidval	|- ( G e. GrpOp -> ( GId ` G ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
4		simpl	|- ( ( ( u G x ) = x /\ ( x G u ) = x ) -> ( u G x ) = x )
5	4	ralimi	|- ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X ( u G x ) = x )
6	5	rgenw	|- A. u e. X ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X ( u G x ) = x )
7	6	a1i	|- ( G e. GrpOp -> A. u e. X ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X ( u G x ) = x ) )
8	1	grpoidinv	|- ( G e. GrpOp -> E. u e. X A. x e. X ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) )
9		simpl	|- ( ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) -> ( ( u G x ) = x /\ ( x G u ) = x ) )
10	9	ralimi	|- ( A. x e. X ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) -> A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
11	10	reximi	|- ( E. u e. X A. x e. X ( ( ( u G x ) = x /\ ( x G u ) = x ) /\ E. y e. X ( ( y G x ) = u /\ ( x G y ) = u ) ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
12	8 11	syl	|- ( G e. GrpOp -> E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) )
13	1	grpoideu	|- ( G e. GrpOp -> E! u e. X A. x e. X ( u G x ) = x )
14	7 12 13	3jca	|- ( G e. GrpOp -> ( A. u e. X ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X ( u G x ) = x ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ E! u e. X A. x e. X ( u G x ) = x ) )
15		reupick2	|- ( ( ( A. u e. X ( A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) -> A. x e. X ( u G x ) = x ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) /\ E! u e. X A. x e. X ( u G x ) = x ) /\ u e. X ) -> ( A. x e. X ( u G x ) = x <-> A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
16	14 15	sylan	|- ( ( G e. GrpOp /\ u e. X ) -> ( A. x e. X ( u G x ) = x <-> A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
17	16	riotabidva	|- ( G e. GrpOp -> ( iota_ u e. X A. x e. X ( u G x ) = x ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
18	3 17	eqtr4d	|- ( G e. GrpOp -> ( GId ` G ) = ( iota_ u e. X A. x e. X ( u G x ) = x ) )
19	2 18	syl5eq	|- ( G e. GrpOp -> U = ( iota_ u e. X A. x e. X ( u G x ) = x ) )