Metamath Proof Explorer


Theorem brgic

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

Ref Expression
Assertion brgic ( 𝑅𝑔 𝑆 ↔ ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 df-gic 𝑔 = ( GrpIso “ ( V ∖ 1o ) )
2 gimfn GrpIso Fn ( Grp × Grp )
3 1 2 brwitnlem ( 𝑅𝑔 𝑆 ↔ ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )