Metamath Proof Explorer

Theorem gimfn

Description: The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015)

Ref Expression
Assertion gimfn 
|- GrpIso Fn ( Grp X. Grp )

Proof

Step Hyp Ref Expression
1 df-gim 
 |-  GrpIso = ( s e. Grp , t e. Grp |-> { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } )
2 ovex 
 |-  ( s GrpHom t ) e. _V
3 2 rabex 
 |-  { g e. ( s GrpHom t ) | g : ( Base ` s ) -1-1-onto-> ( Base ` t ) } e. _V
4 1 3 fnmpoi 
 |-  GrpIso Fn ( Grp X. Grp )