Metamath Proof Explorer


Theorem invf

Description: The inverse relation is a function from isomorphisms to isomorphisms. (Contributed by Mario Carneiro, 2-Jan-2017)

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

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 invfval.x
 |-  ( ph -> X e. B )
5 invfval.y
 |-  ( ph -> Y e. B )
6 isoval.n
 |-  I = ( Iso ` C )
7 1 2 3 4 5 invfun
 |-  ( ph -> Fun ( X N Y ) )
8 7 funfnd
 |-  ( ph -> ( X N Y ) Fn dom ( X N Y ) )
9 1 2 3 4 5 6 isoval
 |-  ( ph -> ( X I Y ) = dom ( X N Y ) )
10 9 fneq2d
 |-  ( ph -> ( ( X N Y ) Fn ( X I Y ) <-> ( X N Y ) Fn dom ( X N Y ) ) )
11 8 10 mpbird
 |-  ( ph -> ( X N Y ) Fn ( X I Y ) )
12 df-rn
 |-  ran ( X N Y ) = dom `' ( X N Y )
13 1 2 3 4 5 invsym2
 |-  ( ph -> `' ( X N Y ) = ( Y N X ) )
14 13 dmeqd
 |-  ( ph -> dom `' ( X N Y ) = dom ( Y N X ) )
15 1 2 3 5 4 6 isoval
 |-  ( ph -> ( Y I X ) = dom ( Y N X ) )
16 14 15 eqtr4d
 |-  ( ph -> dom `' ( X N Y ) = ( Y I X ) )
17 12 16 eqtrid
 |-  ( ph -> ran ( X N Y ) = ( Y I X ) )
18 eqimss
 |-  ( ran ( X N Y ) = ( Y I X ) -> ran ( X N Y ) C_ ( Y I X ) )
19 17 18 syl
 |-  ( ph -> ran ( X N Y ) C_ ( Y I X ) )
20 df-f
 |-  ( ( X N Y ) : ( X I Y ) --> ( Y I X ) <-> ( ( X N Y ) Fn ( X I Y ) /\ ran ( X N Y ) C_ ( Y I X ) ) )
21 11 19 20 sylanbrc
 |-  ( ph -> ( X N Y ) : ( X I Y ) --> ( Y I X ) )