Metamath Proof Explorer


Theorem inviso2

Description: If G is an inverse to F , then G is an isomorphism. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses invfval.b B=BaseC
invfval.n N=InvC
invfval.c φCCat
invfval.x φXB
invfval.y φYB
isoval.n I=IsoC
inviso1.1 φFXNYG
Assertion inviso2 φGYIX

Proof

Step Hyp Ref Expression
1 invfval.b B=BaseC
2 invfval.n N=InvC
3 invfval.c φCCat
4 invfval.x φXB
5 invfval.y φYB
6 isoval.n I=IsoC
7 inviso1.1 φFXNYG
8 1 2 3 4 5 invsym φFXNYGGYNXF
9 7 8 mpbid φGYNXF
10 1 2 3 5 4 6 9 inviso1 φGYIX