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 φ C Cat
invisoinv.x φ X B
invisoinv.y φ Y B
invisoinv.f φ F X I Y
Assertion invisoinvl φ 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 φ C Cat
5 invisoinv.x φ X B
6 invisoinv.y φ Y B
7 invisoinv.f φ F X I Y
8 eqid comp C = comp C
9 eqid Id C = Id C
10 1 9 4 6 idiso φ Id C Y Y Iso C Y
11 2 a1i φ I = Iso C
12 11 oveqd φ Y I Y = Y Iso C Y
13 10 12 eleqtrrd φ Id C Y Y I Y
14 1 3 4 5 6 2 7 8 6 13 invco φ 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 φ X I Y X Hom C Y
17 16 7 sseldd φ F X Hom C Y
18 1 15 9 4 5 8 6 17 catlid φ Id C Y X Y comp C Y F = F
19 3 a1i φ N = Inv C
20 19 oveqd φ Y N Y = Y Inv C Y
21 20 fveq1d φ Y N Y Id C Y = Y Inv C Y Id C Y
22 1 9 4 6 idinv φ Y Inv C Y Id C Y = Id C Y
23 21 22 eqtrd φ Y N Y Id C Y = Id C Y
24 23 oveq2d φ 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 φ Y I X Y Hom C X
26 1 3 4 5 6 2 invf φ X N Y : X I Y Y I X
27 26 7 ffvelrnd φ X N Y F Y I X
28 25 27 sseldd φ X N Y F Y Hom C X
29 1 15 9 4 6 8 5 28 catrid φ X N Y F Y Y comp C X Id C Y = X N Y F
30 24 29 eqtrd φ X N Y F Y Y comp C X Y N Y Id C Y = X N Y F
31 14 18 30 3brtr3d φ F X N Y X N Y F
32 1 3 4 6 5 invsym φ X N Y F Y N X F F X N Y X N Y F
33 31 32 mpbird φ X N Y F Y N X F