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

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 
|- ( ph -> C e. Cat )
invss.x 
|- ( ph -> X e. B )
invss.y 
|- ( ph -> Y e. B )
invss.h 
|- H = ( Hom ` C )
Assertion invss 
|- ( ph -> ( X N Y ) C_ ( ( X H Y ) X. ( Y H 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 invss.x 
 |-  ( ph -> X e. B )
5 invss.y 
 |-  ( ph -> Y e. B )
6 invss.h 
 |-  H = ( Hom ` C )
7 eqid 
 |-  ( Sect ` C ) = ( Sect ` C )
8 1 2 3 4 5 7 invfval 
 |-  ( ph -> ( X N Y ) = ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) )
9 inss1 
 |-  ( ( X ( Sect ` C ) Y ) i^i `' ( Y ( Sect ` C ) X ) ) C_ ( X ( Sect ` C ) Y )
10 8 9 eqsstrdi 
 |-  ( ph -> ( X N Y ) C_ ( 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 
 |-  ( ph -> ( X ( Sect ` C ) Y ) C_ ( ( X H Y ) X. ( Y H X ) ) )
14 10 13 sstrd 
 |-  ( ph -> ( X N Y ) C_ ( ( X H Y ) X. ( Y H X ) ) )