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

Metamath Proof Explorer

Theorem invinv

Description: The inverse of the inverse of an isomorphism is itself. Proposition 3.14(1) of Adamek p. 29. (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 )
invss.x 
|- ( ph -> X e. B )
invss.y 
|- ( ph -> Y e. B )
isoval.n 
|- I = ( Iso ` C )
invinv.f 
|- ( ph -> F e. ( X I Y ) )
Assertion invinv 
|- ( ph -> ( ( Y N X ) ` ( ( X N Y ) ` F ) ) = F )

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 invinv.f 
 |-  ( ph -> F e. ( X I Y ) )
8 1 2 3 4 5 invsym2 
 |-  ( ph -> `' ( X N Y ) = ( Y N X ) )
9 8 fveq1d 
 |-  ( ph -> ( `' ( X N Y ) ` ( ( X N Y ) ` F ) ) = ( ( Y N X ) ` ( ( X N Y ) ` F ) ) )
10 1 2 3 4 5 6 invf1o 
 |-  ( ph -> ( X N Y ) : ( X I Y ) -1-1-onto-> ( Y I X ) )
11 f1ocnvfv1 
 |-  ( ( ( X N Y ) : ( X I Y ) -1-1-onto-> ( Y I X ) /\ F e. ( X I Y ) ) -> ( `' ( X N Y ) ` ( ( X N Y ) ` F ) ) = F )
12 10 7 11 syl2anc 
 |-  ( ph -> ( `' ( X N Y ) ` ( ( X N Y ) ` F ) ) = F )
13 9 12 eqtr3d 
 |-  ( ph -> ( ( Y N X ) ` ( ( X N Y ) ` F ) ) = F )