Metamath Proof Explorer


Theorem invss

Description: The inverse relation is a relation between morphisms F : X --> Y and their inverses G : Y --> X . (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses invfval.b B = Base C
invfval.n N = Inv C
invfval.c φ C Cat
invfval.x φ X B
invfval.y φ Y B
invss.h H = Hom C
Assertion invss φ X N Y X H Y × Y H X

Proof

Step Hyp Ref Expression
1 invfval.b B = Base C
2 invfval.n N = Inv C
3 invfval.c φ C Cat
4 invfval.x φ X B
5 invfval.y φ Y B
6 invss.h H = Hom C
7 eqid Sect C = Sect C
8 1 2 3 4 5 7 invfval φ X N Y = X Sect C Y Y Sect C X -1
9 inss1 X Sect C Y Y Sect C X -1 X Sect C Y
10 8 9 eqsstrdi φ X N Y X Sect C Y
11 eqid comp C = comp C
12 eqid Id C = Id C
13 1 6 11 12 7 3 4 5 sectss φ X Sect C Y X H Y × Y H X
14 10 13 sstrd φ X N Y X H Y × Y H X