Metamath Proof Explorer


Theorem gicrcl

Description: Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion gicrcl
|- ( R ~=g S -> S e. Grp )

Proof

Step Hyp Ref Expression
1 brgic
 |-  ( R ~=g S <-> ( R GrpIso S ) =/= (/) )
2 n0
 |-  ( ( R GrpIso S ) =/= (/) <-> E. f f e. ( R GrpIso S ) )
3 1 2 bitri
 |-  ( R ~=g S <-> E. f f e. ( R GrpIso S ) )
4 gimghm
 |-  ( f e. ( R GrpIso S ) -> f e. ( R GrpHom S ) )
5 ghmgrp2
 |-  ( f e. ( R GrpHom S ) -> S e. Grp )
6 4 5 syl
 |-  ( f e. ( R GrpIso S ) -> S e. Grp )
7 6 exlimiv
 |-  ( E. f f e. ( R GrpIso S ) -> S e. Grp )
8 3 7 sylbi
 |-  ( R ~=g S -> S e. Grp )