Metamath Proof Explorer


Theorem brgici

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

Ref Expression
Assertion brgici ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑅𝑔 𝑆 )

Proof

Step Hyp Ref Expression
1 ne0i ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )
2 brgic ( 𝑅𝑔 𝑆 ↔ ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )
3 1 2 sylibr ( 𝐹 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑅𝑔 𝑆 )