Theorem oyoncl

Description: The opposite Yoneda embedding is a functor from oppCatC to the functor category C -> SetCat . (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Hypotheses	oyoncl.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oyoncl.y	$$⊢Y=\mathrm{Yon}\left(O\right)$$
	oyoncl.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	oyoncl.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
	oyoncl.u	$$⊢\phi \to U\in V$$
	oyoncl.h	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\subseteq U$$
	oyoncl.q	$$⊢Q=C\mathrm{FuncCat}S$$
Assertion	oyoncl	$$⊢\phi \to Y\in \left(O\mathrm{Func}Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		oyoncl.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oyoncl.y	$$⊢Y=\mathrm{Yon}\left(O\right)$$
3		oyoncl.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		oyoncl.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
5		oyoncl.u	$$⊢\phi \to U\in V$$
6		oyoncl.h	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\subseteq U$$
7		oyoncl.q	$$⊢Q=C\mathrm{FuncCat}S$$
8	1	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
9	3 8	syl	$$⊢\phi \to O\in \mathrm{Cat}$$
10		eqid	$$⊢\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(O\right)$$
11		eqid	$$⊢\mathrm{oppCat}\left(O\right)\mathrm{FuncCat}S=\mathrm{oppCat}\left(O\right)\mathrm{FuncCat}S$$
12		eqid	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(C\right)$$
13	1 12	oppchomf	$$⊢tpos{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
14	13	rneqi	$$⊢\mathrm{ran}tpos{\mathrm{Hom}}_{𝑓}\left(C\right)=\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(O\right)$$
15		relxp	$$⊢\mathrm{Rel}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
16		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
17	12 16	homffn	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)Fn\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
18	17	fndmi	$$⊢\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Base}}_C\times {\mathrm{Base}}_C$$
19	18	releqi	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)\leftrightarrow \mathrm{Rel}\left({\mathrm{Base}}_C\times {\mathrm{Base}}_C\right)$$
20	15 19	mpbir	$$⊢\mathrm{Rel}\mathrm{dom}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
21		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)$$
22	20 21	ax-mp	$$⊢\mathrm{ran}tpos{\mathrm{Hom}}_{𝑓}\left(C\right)=\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
23	14 22	eqtr3i	$$⊢\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(O\right)=\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
24	23 6	eqsstrid	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(O\right)\subseteq U$$
25	2 9 10 4 11 5 24	yoncl	$$⊢\phi \to Y\in \left(O\mathrm{Func}\left(\mathrm{oppCat}\left(O\right)\mathrm{FuncCat}S\right)\right)$$
26	1	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
27	26	a1i	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
28	1	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
29	28	a1i	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
30		eqidd	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(S\right)={\mathrm{Hom}}_{𝑓}\left(S\right)$$
31		eqidd	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(S\right)={\mathrm{comp}}_{𝑓}\left(S\right)$$
32	10	oppccat	$$⊢O\in \mathrm{Cat}\to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
33	9 32	syl	$$⊢\phi \to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
34	4	setccat	$$⊢U\in V\to S\in \mathrm{Cat}$$
35	5 34	syl	$$⊢\phi \to S\in \mathrm{Cat}$$
36	27 29 30 31 3 33 35 35	fucpropd	$$⊢\phi \to C\mathrm{FuncCat}S=\mathrm{oppCat}\left(O\right)\mathrm{FuncCat}S$$
37	7 36	syl5eq	$$⊢\phi \to Q=\mathrm{oppCat}\left(O\right)\mathrm{FuncCat}S$$
38	37	oveq2d	$$⊢\phi \to O\mathrm{Func}Q=O\mathrm{Func}\left(\mathrm{oppCat}\left(O\right)\mathrm{FuncCat}S\right)$$
39	25 38	eleqtrrd	$$⊢\phi \to Y\in \left(O\mathrm{Func}Q\right)$$