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

Definition df-gid 20875
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 20870 . 2  class GId
2 vg . . 3  set  g
3 cvv 2801 . . 3  class  _V
4 vu . . . . . . . . 9  set  u
54cv 1631 . . . . . . . 8  class  u
6 vx . . . . . . . . 9  set  x
76cv 1631 . . . . . . . 8  class  x
82cv 1631 . . . . . . . 8  class  g
95, 7, 8co 5874 . . . . . . 7  class  ( u g x )
109, 7wceq 1632 . . . . . 6  wff  ( u g x )  =  x
117, 5, 8co 5874 . . . . . . 7  class  ( x g u )
1211, 7wceq 1632 . . . . . 6  wff  ( x g u )  =  x
1310, 12wa 358 . . . . 5  wff  ( ( u g x )  =  x  /\  (
x g u )  =  x )
148crn 4706 . . . . 5  class  ran  g
1513, 6, 14wral 2556 . . . 4  wff  A. x  e.  ran  g ( ( u g x )  =  x  /\  (
x g u )  =  x )
1615, 4, 14crio 6313 . . 3  class  ( iota_ u  e.  ran  g A. x  e.  ran  g ( ( u g x )  =  x  /\  ( x g u )  =  x ) )
172, 3, 16cmpt 4093 . 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 1632 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  20896  fngid  20897
  Copyright terms: Public domain W3C validator