This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem inviso1

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

Ref Expression
Hypotheses invfval.b 
|- B = ( Base ` C )
invfval.n 
|- N = ( Inv ` C )
invfval.c 
|- ( ph -> C e. Cat )
invss.x 
|- ( ph -> X e. B )
invss.y 
|- ( ph -> Y e. B )
isoval.n 
|- I = ( Iso ` C )
inviso1.1 
|- ( ph -> F ( X N Y ) G )
Assertion inviso1 
|- ( ph -> F e. ( X I Y ) )

Proof

Step Hyp Ref Expression
1 invfval.b 
 |-  B = ( Base ` C )
2 invfval.n 
 |-  N = ( Inv ` C )
3 invfval.c 
 |-  ( ph -> C e. Cat )
4 invss.x 
 |-  ( ph -> X e. B )
5 invss.y 
 |-  ( ph -> Y e. B )
6 isoval.n 
 |-  I = ( Iso ` C )
7 inviso1.1 
 |-  ( ph -> F ( X N Y ) G )
8 1 2 3 4 5 invfun 
 |-  ( ph -> Fun ( X N Y ) )
9 funrel 
 |-  ( Fun ( X N Y ) -> Rel ( X N Y ) )
10 8 9 syl 
 |-  ( ph -> Rel ( X N Y ) )
11 releldm 
 |-  ( ( Rel ( X N Y ) /\ F ( X N Y ) G ) -> F e. dom ( X N Y ) )
12 10 7 11 syl2anc 
 |-  ( ph -> F e. dom ( X N Y ) )
13 1 2 3 4 5 6 isoval 
 |-  ( ph -> ( X I Y ) = dom ( X N Y ) )
14 12 13 eleqtrrd 
 |-  ( ph -> F e. ( X I Y ) )