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

Definition df-gim 16506
Description: An isomorphism of groups is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group operation. (Contributed by Stefan O'Rear, 21-Jan-2015.)
Assertion
Ref Expression
df-gim  |- GrpIso  =  ( s  e.  Grp , 
t  e.  Grp  |->  { g  e.  ( s 
GrpHom  t )  |  g : ( Base `  s
)
-1-1-onto-> ( Base `  t ) } )
Distinct variable group:    g, s, t

Detailed syntax breakdown of Definition df-gim
StepHypRef Expression
1 cgim 16504 . 2  class GrpIso
2 vs . . 3  setvar  s
3 vt . . 3  setvar  t
4 cgrp 16252 . . 3  class  Grp
52cv 1397 . . . . . 6  class  s
6 cbs 14716 . . . . . 6  class  Base
75, 6cfv 5570 . . . . 5  class  ( Base `  s )
83cv 1397 . . . . . 6  class  t
98, 6cfv 5570 . . . . 5  class  ( Base `  t )
10 vg . . . . . 6  setvar  g
1110cv 1397 . . . . 5  class  g
127, 9, 11wf1o 5569 . . . 4  wff  g : ( Base `  s
)
-1-1-onto-> ( Base `  t )
13 cghm 16463 . . . . 5  class  GrpHom
145, 8, 13co 6270 . . . 4  class  ( s 
GrpHom  t )
1512, 10, 14crab 2808 . . 3  class  { g  e.  ( s  GrpHom  t )  |  g : ( Base `  s
)
-1-1-onto-> ( Base `  t ) }
162, 3, 4, 4, 15cmpt2 6272 . 2  class  ( s  e.  Grp ,  t  e.  Grp  |->  { g  e.  ( s  GrpHom  t )  |  g : ( Base `  s
)
-1-1-onto-> ( Base `  t ) } )
171, 16wceq 1398 1  wff GrpIso  =  ( s  e.  Grp , 
t  e.  Grp  |->  { g  e.  ( s 
GrpHom  t )  |  g : ( Base `  s
)
-1-1-onto-> ( Base `  t ) } )
Colors of variables: wff setvar class
This definition is referenced by:  gimfn  16508  isgim  16509
  Copyright terms: Public domain W3C validator