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

Definition df-giso 21027
Description: Define the set of group isomorphisms from  g to  h. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-giso  |-  GrpOpIso  =  ( g  e.  GrpOp ,  h  e.  GrpOp  |->  { f  e.  ( g GrpOpHom  h )  |  f : ran  g
-1-1-onto-> ran  h } )
Distinct variable group:    f, g, h

Detailed syntax breakdown of Definition df-giso
StepHypRef Expression
1 cgiso 21026 . 2  class  GrpOpIso
2 vg . . 3  set  g
3 vh . . 3  set  h
4 cgr 20853 . . 3  class  GrpOp
52cv 1622 . . . . . 6  class  g
65crn 4690 . . . . 5  class  ran  g
73cv 1622 . . . . . 6  class  h
87crn 4690 . . . . 5  class  ran  h
9 vf . . . . . 6  set  f
109cv 1622 . . . . 5  class  f
116, 8, 10wf1o 5254 . . . 4  wff  f : ran  g -1-1-onto-> ran  h
12 cghom 21024 . . . . 5  class GrpOpHom
135, 7, 12co 5858 . . . 4  class  ( g GrpOpHom  h )
1411, 9, 13crab 2547 . . 3  class  { f  e.  ( g GrpOpHom  h
)  |  f : ran  g -1-1-onto-> ran  h }
152, 3, 4, 4, 14cmpt2 5860 . 2  class  ( g  e.  GrpOp ,  h  e. 
GrpOp  |->  { f  e.  ( g GrpOpHom  h )  |  f : ran  g
-1-1-onto-> ran  h } )
161, 15wceq 1623 1  wff  GrpOpIso  =  ( g  e.  GrpOp ,  h  e.  GrpOp  |->  { f  e.  ( g GrpOpHom  h )  |  f : ran  g
-1-1-onto-> ran  h } )
Colors of variables: wff set class
This definition is referenced by:  elgiso  24003
  Copyright terms: Public domain W3C validator