gicrcl

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

		Ref	Expression
	Assertion	gicrcl	$⊢ R ≃_{𝑔} S \to S \in Grp$

Step	Hyp	Ref	Expression
1		brgic	$⊢ R ≃_{𝑔} S \leftrightarrow R GrpIso S \neq \emptyset$
2		n0	$⊢ R GrpIso S \neq \emptyset \leftrightarrow \exists f f \in (R GrpIso S)$
3	1 2	bitri	$⊢ R ≃_{𝑔} S \leftrightarrow \exists f f \in (R GrpIso S)$
4		gimghm	$⊢ f \in (R GrpIso S) \to f \in (R GrpHom S)$
5		ghmgrp2	$⊢ f \in (R GrpHom S) \to S \in Grp$
6	4 5	syl	$⊢ f \in (R GrpIso S) \to S \in Grp$
7	6	exlimiv	$⊢ \exists f f \in (R GrpIso S) \to S \in Grp$
8	3 7	sylbi	$⊢ R ≃_{𝑔} S \to S \in Grp$

Metamath Proof Explorer