MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gid Unicode version

Definition df-gid 20859
Description: Define a function that maps a group operation to the group's identity element. (Contributed by FL, 5-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.)
Assertion
Ref Expression
df-gid  |- GId  =  ( g  e.  _V  |->  (
iota_ u  e.  ran  g A. x  e.  ran  g ( ( u g x )  =  x  /\  ( x g u )  =  x ) ) )
Distinct variable group:    u, g, x

Detailed syntax breakdown of Definition df-gid
StepHypRef Expression
1 cgi 20854 . 2  class GId
2 vg . . 3  set  g
3 cvv 2788 . . 3  class  _V
4 vu . . . . . . . . 9  set  u
54cv 1622 . . . . . . . 8  class  u
6 vx . . . . . . . . 9  set  x
76cv 1622 . . . . . . . 8  class  x
82cv 1622 . . . . . . . 8  class  g
95, 7, 8co 5858 . . . . . . 7  class  ( u g x )
109, 7wceq 1623 . . . . . 6  wff  ( u g x )  =  x
117, 5, 8co 5858 . . . . . . 7  class  ( x g u )
1211, 7wceq 1623 . . . . . 6  wff  ( x g u )  =  x
1310, 12wa 358 . . . . 5  wff  ( ( u g x )  =  x  /\  (
x g u )  =  x )
148crn 4690 . . . . 5  class  ran  g
1513, 6, 14wral 2543 . . . 4  wff  A. x  e.  ran  g ( ( u g x )  =  x  /\  (
x g u )  =  x )
1615, 4, 14crio 6297 . . 3  class  ( iota_ u  e.  ran  g A. x  e.  ran  g ( ( u g x )  =  x  /\  ( x g u )  =  x ) )
172, 3, 16cmpt 4077 . 2  class  ( g  e.  _V  |->  ( iota_ u  e.  ran  g A. x  e.  ran  g ( ( u g x )  =  x  /\  ( x g u )  =  x ) ) )
181, 17wceq 1623 1  wff GId  =  ( g  e.  _V  |->  (
iota_ u  e.  ran  g A. x  e.  ran  g ( ( u g x )  =  x  /\  ( x g u )  =  x ) ) )
Colors of variables: wff set class
This definition is referenced by:  gidval  20880  fngid  20881
  Copyright terms: Public domain W3C validator