This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	eqtrid	\|- ( G e. GrpOp -> U = ( iota_ u e. X A. x e. X ( u G x ) = x ) )