Theorem oppcinv

Description: An inverse in the opposite category. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	oppcsect.b	$$⊢B={\mathrm{Base}}_C$$
	oppcsect.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppcsect.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	oppcsect.x	$$⊢\phi \to X\in B$$
	oppcsect.y	$$⊢\phi \to Y\in B$$
	oppcinv.s	$$⊢I=\mathrm{Inv}\left(C\right)$$
	oppcinv.t	$$⊢J=\mathrm{Inv}\left(O\right)$$
Assertion	oppcinv	$$⊢\phi \to XJY=YIX$$

Proof

Step	Hyp	Ref	Expression
1		oppcsect.b	$$⊢B={\mathrm{Base}}_C$$
2		oppcsect.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
3		oppcsect.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		oppcsect.x	$$⊢\phi \to X\in B$$
5		oppcsect.y	$$⊢\phi \to Y\in B$$
6		oppcinv.s	$$⊢I=\mathrm{Inv}\left(C\right)$$
7		oppcinv.t	$$⊢J=\mathrm{Inv}\left(O\right)$$
8		incom	$$⊢\left(X\mathrm{Sect}\left(O\right)Y\right)\cap {\left(Y\mathrm{Sect}\left(O\right)X\right)}^{-1}={\left(Y\mathrm{Sect}\left(O\right)X\right)}^{-1}\cap \left(X\mathrm{Sect}\left(O\right)Y\right)$$
9		eqid	$$⊢\mathrm{Sect}\left(C\right)=\mathrm{Sect}\left(C\right)$$
10		eqid	$$⊢\mathrm{Sect}\left(O\right)=\mathrm{Sect}\left(O\right)$$
11	1 2 3 5 4 9 10	oppcsect2	$$⊢\phi \to Y\mathrm{Sect}\left(O\right)X={\left(Y\mathrm{Sect}\left(C\right)X\right)}^{-1}$$
12	11	cnveqd	$$⊢\phi \to {\left(Y\mathrm{Sect}\left(O\right)X\right)}^{-1}={{\left(Y\mathrm{Sect}\left(C\right)X\right)}^{-1}}^{-1}$$
13		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
14		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
15		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
16	1 13 14 15 9 3 5 4	sectss	$$⊢\phi \to Y\mathrm{Sect}\left(C\right)X\subseteq \left(Y\mathrm{Hom}\left(C\right)X\right)\times \left(X\mathrm{Hom}\left(C\right)Y\right)$$
17		relxp	$$⊢\mathrm{Rel}\left(\left(Y\mathrm{Hom}\left(C\right)X\right)\times \left(X\mathrm{Hom}\left(C\right)Y\right)\right)$$
18		relss	$$⊢Y\mathrm{Sect}\left(C\right)X\subseteq \left(Y\mathrm{Hom}\left(C\right)X\right)\times \left(X\mathrm{Hom}\left(C\right)Y\right)\to \left(\mathrm{Rel}\left(\left(Y\mathrm{Hom}\left(C\right)X\right)\times \left(X\mathrm{Hom}\left(C\right)Y\right)\right)\to \mathrm{Rel}\left(Y\mathrm{Sect}\left(C\right)X\right)\right)$$
19	16 17 18	mpisyl	$$⊢\phi \to \mathrm{Rel}\left(Y\mathrm{Sect}\left(C\right)X\right)$$
20		dfrel2	$$⊢\mathrm{Rel}\left(Y\mathrm{Sect}\left(C\right)X\right)\leftrightarrow {{\left(Y\mathrm{Sect}\left(C\right)X\right)}^{-1}}^{-1}=Y\mathrm{Sect}\left(C\right)X$$
21	19 20	sylib	$$⊢\phi \to {{\left(Y\mathrm{Sect}\left(C\right)X\right)}^{-1}}^{-1}=Y\mathrm{Sect}\left(C\right)X$$
22	12 21	eqtrd	$$⊢\phi \to {\left(Y\mathrm{Sect}\left(O\right)X\right)}^{-1}=Y\mathrm{Sect}\left(C\right)X$$
23	1 2 3 4 5 9 10	oppcsect2	$$⊢\phi \to X\mathrm{Sect}\left(O\right)Y={\left(X\mathrm{Sect}\left(C\right)Y\right)}^{-1}$$
24	22 23	ineq12d	$$⊢\phi \to {\left(Y\mathrm{Sect}\left(O\right)X\right)}^{-1}\cap \left(X\mathrm{Sect}\left(O\right)Y\right)=\left(Y\mathrm{Sect}\left(C\right)X\right)\cap {\left(X\mathrm{Sect}\left(C\right)Y\right)}^{-1}$$
25	8 24	syl5eq	$$⊢\phi \to \left(X\mathrm{Sect}\left(O\right)Y\right)\cap {\left(Y\mathrm{Sect}\left(O\right)X\right)}^{-1}=\left(Y\mathrm{Sect}\left(C\right)X\right)\cap {\left(X\mathrm{Sect}\left(C\right)Y\right)}^{-1}$$
26	2 1	oppcbas	$$⊢B={\mathrm{Base}}_O$$
27	2	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
28	3 27	syl	$$⊢\phi \to O\in \mathrm{Cat}$$
29	26 7 28 4 5 10	invfval	$$⊢\phi \to XJY=\left(X\mathrm{Sect}\left(O\right)Y\right)\cap {\left(Y\mathrm{Sect}\left(O\right)X\right)}^{-1}$$
30	1 6 3 5 4 9	invfval	$$⊢\phi \to YIX=\left(Y\mathrm{Sect}\left(C\right)X\right)\cap {\left(X\mathrm{Sect}\left(C\right)Y\right)}^{-1}$$
31	25 29 30	3eqtr4d	$$⊢\phi \to XJY=YIX$$