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 𝑔 S S Grp

Proof

Step Hyp Ref Expression
1 brgic R 𝑔 S R GrpIso S
2 n0 R GrpIso S f f R GrpIso S
3 1 2 bitri R 𝑔 S f f R GrpIso S
4 gimghm f R GrpIso S f R GrpHom S
5 ghmgrp2 f R GrpHom S S Grp
6 4 5 syl f R GrpIso S S Grp
7 6 exlimiv f f R GrpIso S S Grp
8 3 7 sylbi R 𝑔 S S Grp