Theorem oppchofcl

Description: Closure of the opposite Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017)

	Ref	Expression
Hypotheses	oppchofcl.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppchofcl.m	$$⊢M={Hom}_F\left(O\right)$$
	oppchofcl.d	$$⊢D=\mathrm{SetCat}\left(U\right)$$
	oppchofcl.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	oppchofcl.u	$$⊢\phi \to U\in V$$
	oppchofcl.h	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\subseteq U$$
Assertion	oppchofcl	$$⊢\phi \to M\in \left(\left(C{\times }_{c}O\right)\mathrm{Func}D\right)$$

Proof

Step	Hyp	Ref	Expression
1		oppchofcl.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppchofcl.m	$$⊢M={Hom}_F\left(O\right)$$
3		oppchofcl.d	$$⊢D=\mathrm{SetCat}\left(U\right)$$
4		oppchofcl.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		oppchofcl.u	$$⊢\phi \to U\in V$$
6		oppchofcl.h	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\subseteq U$$
7		eqid	$$⊢\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(O\right)$$
8	1	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
9	4 8	syl	$$⊢\phi \to O\in \mathrm{Cat}$$
10		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
11	1 10	oppchomf	$$⊢tpos{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
12	11	rneqi	$$⊢\mathrm{ran}tpos{\mathrm{Hom}}_{𝑓}\left(C\right)=\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(O\right)$$
13		relxp	$$⊢\mathrm{Rel}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
14		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
15	10 14	homffn	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
16	15	fndmi	$$⊢\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Base}}_C\times {\mathrm{Base}}_C$$
17	16	releqi	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)\leftrightarrow \mathrm{Rel}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
18	13 17	mpbir	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
19		rntpos	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)\to \mathrm{ran}tpos{\mathrm{Hom}}_{𝑓}\left(C\right)=\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
20	18 19	ax-mp	$$⊢\mathrm{ran}tpos{\mathrm{Hom}}_{𝑓}\left(C\right)=\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
21	12 20	eqtr3i	$$⊢\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(O\right)=\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
22	21 6	eqsstrid	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(O\right)\subseteq U$$
23	2 7 3 9 5 22	hofcl	$$⊢\phi \to M\in \left(\left(\mathrm{oppCat}\left(O\right){\times }_{c}O\right)\mathrm{Func}D\right)$$
24	1	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
25	24	a1i	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
26	1	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
27	26	a1i	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
28		eqidd	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(O\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
29		eqidd	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(O\right)={\mathrm{comp}}_{𝑓}\left(O\right)$$
30	7	oppccat	$$⊢O\in \mathrm{Cat}\to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
31	9 30	syl	$$⊢\phi \to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
32	25 27 28 29 4 31 9 9	xpcpropd	$$⊢\phi \to C{\times }_{c}O=\mathrm{oppCat}\left(O\right){\times }_{c}O$$
33	32	oveq1d	$$⊢\phi \to \left(C{\times }_{c}O\right)\mathrm{Func}D=\left(\mathrm{oppCat}\left(O\right){\times }_{c}O\right)\mathrm{Func}D$$
34	23 33	eleqtrrd	$$⊢\phi \to M\in \left(\left(C{\times }_{c}O\right)\mathrm{Func}D\right)$$