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={\mathrm{Base}}_C$$
	invfval.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
	invfval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	invfval.x	$$⊢\phi \to X\in B$$
	invfval.y	$$⊢\phi \to Y\in B$$
	invss.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
Assertion	invss	$$⊢\phi \to XNY\subseteq \left(XHY\right)\times \left(YHX\right)$$

Proof

Step	Hyp	Ref	Expression
1		invfval.b	$$⊢B={\mathrm{Base}}_C$$
2		invfval.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
3		invfval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		invfval.x	$$⊢\phi \to X\in B$$
5		invfval.y	$$⊢\phi \to Y\in B$$
6		invss.h	$$⊢H=\mathrm{Hom}\left(C\right)$$
7		eqid	$$⊢\mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(C\right)$$
8	1 2 3 4 5 7	invfval	$$⊢\phi \to XNY=\left(X\mathrm{Sect}\left(C\right)Y\right)\cap {\left(Y\mathrm{Sect}\left(C\right)X\right)}^{-1}$$
9		inss1	$$⊢\left(X\mathrm{Sect}\left(C\right)Y\right)\cap {\left(Y\mathrm{Sect}\left(C\right)X\right)}^{-1}\subseteq X\mathrm{Sect}\left(C\right)Y$$
10	8 9	eqsstrdi	$$⊢\phi \to XNY\subseteq X\mathrm{Sect}\left(C\right)Y$$
11		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
12		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
13	1 6 11 12 7 3 4 5	sectss	$$⊢\phi \to X\mathrm{Sect}\left(C\right)Y\subseteq \left(XHY\right)\times \left(YHX\right)$$
14	10 13	sstrd	$$⊢\phi \to XNY\subseteq \left(XHY\right)\times \left(YHX\right)$$