Theorem brgici

Description: Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	brgici	$$⊢F\in \left(R\mathrm{GrpIso}S\right)\to R{\simeq }_{𝑔}S$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢F\in \left(R\mathrm{GrpIso}S\right)\to R\mathrm{GrpIso}S\ne \varnothing$$
2		brgic	$$⊢R{\simeq }_{𝑔}S\leftrightarrow R\mathrm{GrpIso}S\ne \varnothing$$
3	1 2	sylibr	$$⊢F\in \left(R\mathrm{GrpIso}S\right)\to R{\simeq }_{𝑔}S$$