Theorem yonval

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

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

Proof

Step	Hyp	Ref	Expression
1		yonval.y	$$⊢Y=\mathrm{Yon}\left(C\right)$$
2		yonval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
3		yonval.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
4		yonval.m	$$⊢M={Hom}_F\left(O\right)$$
5		df-yon	$$⊢\mathrm{Yon}=\left(c\in \mathrm{Cat}⟼⟨c,\mathrm{oppCat}\left(c\right)⟩{curry}_F{Hom}_F\left(\mathrm{oppCat}\left(c\right)\right)\right)$$
6		simpr	$$⊢\left(\phi \wedge c=C\right)\to c=C$$
7	6	fveq2d	$$⊢\left(\phi \wedge c=C\right)\to \mathrm{oppCat}\left(c\right)=\mathrm{oppCat}\left(C\right)$$
8	7 3	eqtr4di	$$⊢\left(\phi \wedge c=C\right)\to \mathrm{oppCat}\left(c\right)=O$$
9	6 8	opeq12d	$$⊢\left(\phi \wedge c=C\right)\to ⟨c,\mathrm{oppCat}\left(c\right)⟩=⟨C,O⟩$$
10	8	fveq2d	$$⊢\left(\phi \wedge c=C\right)\to {Hom}_F\left(\mathrm{oppCat}\left(c\right)\right)={Hom}_F\left(O\right)$$
11	10 4	eqtr4di	$$⊢\left(\phi \wedge c=C\right)\to {Hom}_F\left(\mathrm{oppCat}\left(c\right)\right)=M$$
12	9 11	oveq12d	$$⊢\left(\phi \wedge c=C\right)\to ⟨c,\mathrm{oppCat}\left(c\right)⟩{curry}_F{Hom}_F\left(\mathrm{oppCat}\left(c\right)\right)=⟨C,O⟩{curry}_{F}M$$
13		ovexd	$$⊢\phi \to ⟨C,O⟩{curry}_{F}M\in \mathrm{V}$$
14	5 12 2 13	fvmptd2	$$⊢\phi \to \mathrm{Yon}\left(C\right)=⟨C,O⟩{curry}_{F}M$$
15	1 14	eqtrid	$$⊢\phi \to Y=⟨C,O⟩{curry}_{F}M$$