Metamath Proof Explorer

Theorem invisoinvl

Description: The inverse of an isomorphism F (which is unique because of invf and is therefore denoted by ( ( X N Y )F ) , see also remark 3.12 in Adamek p. 28) is invers to the isomorphism. (Contributed by AV, 9-Apr-2020)

Ref Expression
Hypotheses invisoinv.b 
|- B = ( Base ` C )
invisoinv.i 
|- I = ( Iso ` C )
invisoinv.n 
|- N = ( Inv ` C )
invisoinv.c 
|- ( ph -> C e. Cat )
invisoinv.x 
|- ( ph -> X e. B )
invisoinv.y 
|- ( ph -> Y e. B )
invisoinv.f 
|- ( ph -> F e. ( X I Y ) )
Assertion invisoinvl 
|- ( ph -> ( ( X N Y ) ` F ) ( Y N X ) F )

Proof

Step Hyp Ref Expression
1 invisoinv.b 
 |-  B = ( Base ` C )
2 invisoinv.i 
 |-  I = ( Iso ` C )
3 invisoinv.n 
 |-  N = ( Inv ` C )
4 invisoinv.c 
 |-  ( ph -> C e. Cat )
5 invisoinv.x 
 |-  ( ph -> X e. B )
6 invisoinv.y 
 |-  ( ph -> Y e. B )
7 invisoinv.f 
 |-  ( ph -> F e. ( X I Y ) )
8 eqid 
 |-  ( comp ` C ) = ( comp ` C )
9 eqid 
 |-  ( Id ` C ) = ( Id ` C )
10 1 9 4 6 idiso 
 |-  ( ph -> ( ( Id ` C ) ` Y ) e. ( Y ( Iso ` C ) Y ) )
11 2 a1i 
 |-  ( ph -> I = ( Iso ` C ) )
12 11 oveqd 
 |-  ( ph -> ( Y I Y ) = ( Y ( Iso ` C ) Y ) )
13 10 12 eleqtrrd 
 |-  ( ph -> ( ( Id ` C ) ` Y ) e. ( Y I Y ) )
14 1 3 4 5 6 2 7 8 6 13 invco 
 |-  ( ph -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) F ) ( X N Y ) ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) ) )
15 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
16 1 15 2 4 5 6 isohom 
 |-  ( ph -> ( X I Y ) C_ ( X ( Hom ` C ) Y ) )
17 16 7 sseldd 
 |-  ( ph -> F e. ( X ( Hom ` C ) Y ) )
18 1 15 9 4 5 8 6 17 catlid 
 |-  ( ph -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) F ) = F )
19 3 a1i 
 |-  ( ph -> N = ( Inv ` C ) )
20 19 oveqd 
 |-  ( ph -> ( Y N Y ) = ( Y ( Inv ` C ) Y ) )
21 20 fveq1d 
 |-  ( ph -> ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) = ( ( Y ( Inv ` C ) Y ) ` ( ( Id ` C ) ` Y ) ) )
22 1 9 4 6 idinv 
 |-  ( ph -> ( ( Y ( Inv ` C ) Y ) ` ( ( Id ` C ) ` Y ) ) = ( ( Id ` C ) ` Y ) )
23 21 22 eqtrd 
 |-  ( ph -> ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) = ( ( Id ` C ) ` Y ) )
24 23 oveq2d 
 |-  ( ph -> ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) ) = ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Id ` C ) ` Y ) ) )
25 1 15 2 4 6 5 isohom 
 |-  ( ph -> ( Y I X ) C_ ( Y ( Hom ` C ) X ) )
26 1 3 4 5 6 2 invf 
 |-  ( ph -> ( X N Y ) : ( X I Y ) --> ( Y I X ) )
27 26 7 ffvelcdmd 
 |-  ( ph -> ( ( X N Y ) ` F ) e. ( Y I X ) )
28 25 27 sseldd 
 |-  ( ph -> ( ( X N Y ) ` F ) e. ( Y ( Hom ` C ) X ) )
29 1 15 9 4 6 8 5 28 catrid 
 |-  ( ph -> ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Id ` C ) ` Y ) ) = ( ( X N Y ) ` F ) )
30 24 29 eqtrd 
 |-  ( ph -> ( ( ( X N Y ) ` F ) ( <. Y , Y >. ( comp ` C ) X ) ( ( Y N Y ) ` ( ( Id ` C ) ` Y ) ) ) = ( ( X N Y ) ` F ) )
31 14 18 30 3brtr3d 
 |-  ( ph -> F ( X N Y ) ( ( X N Y ) ` F ) )
32 1 3 4 6 5 invsym 
 |-  ( ph -> ( ( ( X N Y ) ` F ) ( Y N X ) F <-> F ( X N Y ) ( ( X N Y ) ` F ) ) )
33 31 32 mpbird 
 |-  ( ph -> ( ( X N Y ) ` F ) ( Y N X ) F )