Theorem oppcyon

Description: Value of the opposite Yoneda embedding. (Contributed by Mario Carneiro, 26-Jan-2017)

	Ref	Expression
Hypotheses	oppcyon.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	oppcyon.y	$$⊢Y=\mathrm{Yon}\left(O\right)$$
	oppcyon.m	$$⊢M={Hom}_F\left(C\right)$$
	oppcyon.c	$$⊢\phi \to C\in \mathrm{Cat}$$
Assertion	oppcyon	$$⊢\phi \to Y=⟨O,C⟩{curry}_{F}M$$

Proof

Step	Hyp	Ref	Expression
1		oppcyon.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		oppcyon.y	$$⊢Y=\mathrm{Yon}\left(O\right)$$
3		oppcyon.m	$$⊢M={Hom}_F\left(C\right)$$
4		oppcyon.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5	1	2oppchomf	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
6	5	a1i	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(C\right)={\mathrm{Hom}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
7	1	2oppccomf	$$⊢{\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
8	7	a1i	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(C\right)={\mathrm{comp}}_{𝑓}\left(\mathrm{oppCat}\left(O\right)\right)$$
9	1	oppccat	$$⊢C\in \mathrm{Cat}\to O\in \mathrm{Cat}$$
10	4 9	syl	$$⊢\phi \to O\in \mathrm{Cat}$$
11		eqid	$$⊢\mathrm{oppCat}\left(O\right)=\mathrm{oppCat}\left(O\right)$$
12	11	oppccat	$$⊢O\in \mathrm{Cat}\to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
13	10 12	syl	$$⊢\phi \to \mathrm{oppCat}\left(O\right)\in \mathrm{Cat}$$
14	6 8 4 13	hofpropd	$$⊢\phi \to {Hom}_F\left(C\right)={Hom}_F\left(\mathrm{oppCat}\left(O\right)\right)$$
15	3 14	eqtrid	$$⊢\phi \to M={Hom}_F\left(\mathrm{oppCat}\left(O\right)\right)$$
16	15	oveq2d	$$⊢\phi \to ⟨O,\mathrm{oppCat}\left(O\right)⟩{curry}_{F}M=⟨O,\mathrm{oppCat}\left(O\right)⟩{curry}_F{Hom}_F\left(\mathrm{oppCat}\left(O\right)\right)$$
17		eqidd	$$⊢\phi \to {\mathrm{Hom}}_{𝑓}\left(O\right)={\mathrm{Hom}}_{𝑓}\left(O\right)$$
18		eqidd	$$⊢\phi \to {\mathrm{comp}}_{𝑓}\left(O\right)={\mathrm{comp}}_{𝑓}\left(O\right)$$
19		eqid	$$⊢\mathrm{SetCat}\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\right)=\mathrm{SetCat}\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\right)$$
20		fvex	$$⊢{\mathrm{Hom}}_{𝑓}\left(C\right)\in \mathrm{V}$$
21	20	rnex	$$⊢\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\in \mathrm{V}$$
22	21	a1i	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\in \mathrm{V}$$
23		ssidd	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\subseteq \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)$$
24	3 1 19 4 22 23	hofcl	$$⊢\phi \to M\in \left(\left(O{\times }_{c}C\right)\mathrm{Func}\mathrm{SetCat}\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\right)\right)$$
25	17 18 6 8 10 10 4 13 24	curfpropd	$$⊢\phi \to ⟨O,C⟩{curry}_{F}M=⟨O,\mathrm{oppCat}\left(O\right)⟩{curry}_{F}M$$
26		eqid	$$⊢{Hom}_F\left(\mathrm{oppCat}\left(O\right)\right)={Hom}_F\left(\mathrm{oppCat}\left(O\right)\right)$$
27	2 10 11 26	yonval	$$⊢\phi \to Y=⟨O,\mathrm{oppCat}\left(O\right)⟩{curry}_F{Hom}_F\left(\mathrm{oppCat}\left(O\right)\right)$$
28	16 25 27	3eqtr4rd	$$⊢\phi \to Y=⟨O,C⟩{curry}_{F}M$$