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 )
	invfval.x	|- ( ph -> X e. B )
	invfval.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		invfval.x	|- ( ph -> X e. B )
5		invfval.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 ) ) )