Metamath Proof Explorer

Theorem isgim

Description: An isomorphism of groups is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015)

Ref Expression
Hypotheses isgim.b 
|- B = ( Base ` R )
isgim.c 
|- C = ( Base ` S )
Assertion isgim 
|- ( F e. ( R GrpIso S ) <-> ( F e. ( R GrpHom S ) /\ F : B -1-1-onto-> C ) )

Proof

Step Hyp Ref Expression
1 isgim.b 
 |-  B = ( Base ` R )
2 isgim.c 
 |-  C = ( Base ` S )
3 df-3an 
 |-  ( ( R e. Grp /\ S e. Grp /\ F e. { c e. ( R GrpHom S ) | c : B -1-1-onto-> C } ) <-> ( ( R e. Grp /\ S e. Grp ) /\ F e. { c e. ( R GrpHom S ) | c : B -1-1-onto-> C } ) )
4 df-gim 
 |-  GrpIso = ( a e. Grp , b e. Grp |-> { c e. ( a GrpHom b ) | c : ( Base ` a ) -1-1-onto-> ( Base ` b ) } )
5 ovex 
 |-  ( a GrpHom b ) e. _V
6 5 rabex 
 |-  { c e. ( a GrpHom b ) | c : ( Base ` a ) -1-1-onto-> ( Base ` b ) } e. _V
7 oveq12 
 |-  ( ( a = R /\ b = S ) -> ( a GrpHom b ) = ( R GrpHom S ) )
8 fveq2 
 |-  ( a = R -> ( Base ` a ) = ( Base ` R ) )
9 8 1 eqtr4di 
 |-  ( a = R -> ( Base ` a ) = B )
10 fveq2 
 |-  ( b = S -> ( Base ` b ) = ( Base ` S ) )
11 10 2 eqtr4di 
 |-  ( b = S -> ( Base ` b ) = C )
12 f1oeq23 
 |-  ( ( ( Base ` a ) = B /\ ( Base ` b ) = C ) -> ( c : ( Base ` a ) -1-1-onto-> ( Base ` b ) <-> c : B -1-1-onto-> C ) )
13 9 11 12 syl2an 
 |-  ( ( a = R /\ b = S ) -> ( c : ( Base ` a ) -1-1-onto-> ( Base ` b ) <-> c : B -1-1-onto-> C ) )
14 7 13 rabeqbidv 
 |-  ( ( a = R /\ b = S ) -> { c e. ( a GrpHom b ) | c : ( Base ` a ) -1-1-onto-> ( Base ` b ) } = { c e. ( R GrpHom S ) | c : B -1-1-onto-> C } )
15 4 6 14 elovmpo 
 |-  ( F e. ( R GrpIso S ) <-> ( R e. Grp /\ S e. Grp /\ F e. { c e. ( R GrpHom S ) | c : B -1-1-onto-> C } ) )
16 ghmgrp1 
 |-  ( F e. ( R GrpHom S ) -> R e. Grp )
17 ghmgrp2 
 |-  ( F e. ( R GrpHom S ) -> S e. Grp )
18 16 17 jca 
 |-  ( F e. ( R GrpHom S ) -> ( R e. Grp /\ S e. Grp ) )
19 18 adantr 
 |-  ( ( F e. ( R GrpHom S ) /\ F : B -1-1-onto-> C ) -> ( R e. Grp /\ S e. Grp ) )
20 19 pm4.71ri 
 |-  ( ( F e. ( R GrpHom S ) /\ F : B -1-1-onto-> C ) <-> ( ( R e. Grp /\ S e. Grp ) /\ ( F e. ( R GrpHom S ) /\ F : B -1-1-onto-> C ) ) )
21 f1oeq1 
 |-  ( c = F -> ( c : B -1-1-onto-> C <-> F : B -1-1-onto-> C ) )
22 21 elrab 
 |-  ( F e. { c e. ( R GrpHom S ) | c : B -1-1-onto-> C } <-> ( F e. ( R GrpHom S ) /\ F : B -1-1-onto-> C ) )
23 22 anbi2i 
 |-  ( ( ( R e. Grp /\ S e. Grp ) /\ F e. { c e. ( R GrpHom S ) | c : B -1-1-onto-> C } ) <-> ( ( R e. Grp /\ S e. Grp ) /\ ( F e. ( R GrpHom S ) /\ F : B -1-1-onto-> C ) ) )
24 20 23 bitr4i 
 |-  ( ( F e. ( R GrpHom S ) /\ F : B -1-1-onto-> C ) <-> ( ( R e. Grp /\ S e. Grp ) /\ F e. { c e. ( R GrpHom S ) | c : B -1-1-onto-> C } ) )
25 3 15 24 3bitr4i 
 |-  ( F e. ( R GrpIso S ) <-> ( F e. ( R GrpHom S ) /\ F : B -1-1-onto-> C ) )