Theorem brgic

Description: The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015)

	Ref	Expression
Assertion	brgic	$$⊢R{\simeq }_{𝑔}S\leftrightarrow R\mathrm{GrpIso}S\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-gic	$$⊢{\simeq }_{𝑔}={\mathrm{GrpIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		gimfn	$$⊢\mathrm{GrpIso}Fn\left(\mathrm{Grp}\times \mathrm{Grp}\right)$$
3	1 2	brwitnlem	$$⊢R{\simeq }_{𝑔}S\leftrightarrow R\mathrm{GrpIso}S\ne \varnothing$$