Metamath Proof Explorer


Theorem giclcl

Description: Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion giclcl
|- ( R ~=g S -> R 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 ghmgrp1
 |-  ( f e. ( R GrpHom S ) -> R e. Grp )
6 4 5 syl
 |-  ( f e. ( R GrpIso S ) -> R e. Grp )
7 6 exlimiv
 |-  ( E. f f e. ( R GrpIso S ) -> R e. Grp )
8 3 7 sylbi
 |-  ( R ~=g S -> R e. Grp )