Theorem yonffth

Description: The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category C as a full subcategory of the category Q of presheaves on C . (Contributed by Mario Carneiro, 29-Jan-2017)

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

Proof

Step	Hyp	Ref	Expression
1		yonffth.y	$$⊢Y=\mathrm{Yon}\left(C\right)$$
2		yonffth.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
3		yonffth.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
4		yonffth.q	$$⊢Q=O\mathrm{FuncCat}S$$
5		yonffth.c	$$⊢\phi \to C\in \mathrm{Cat}$$
6		yonffth.u	$$⊢\phi \to U\in V$$
7		yonffth.h	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\subseteq U$$
8		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
9		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
10		eqid	$$⊢\mathrm{SetCat}\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\right)=\mathrm{SetCat}\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\right)$$
11		eqid	$$⊢{Hom}_F\left(Q\right)={Hom}_F\left(Q\right)$$
12		eqid	$$⊢\left(Q{\times }_{c}O\right)\mathrm{FuncCat}\mathrm{SetCat}\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\right)=\left(Q{\times }_{c}O\right)\mathrm{FuncCat}\mathrm{SetCat}\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\right)$$
13		eqid	$$⊢O{eval}_{F}S=O{eval}_{F}S$$
14		eqid	$$⊢{Hom}_F\left(Q\right){\circ }_{\mathrm{func}}\left(\left(⟨1^{st}\left(Y\right),tpos{2}^{nd}\left(Y\right)⟩{\circ }_{\mathrm{func}}\left(Q{2^{nd}}_{F}O\right)\right){⟨,⟩}_F\left(Q{1^{st}}_{F}O\right)\right)={Hom}_F\left(Q\right){\circ }_{\mathrm{func}}\left(\left(⟨1^{st}\left(Y\right),tpos{2}^{nd}\left(Y\right)⟩{\circ }_{\mathrm{func}}\left(Q{2^{nd}}_{F}O\right)\right){⟨,⟩}_F\left(Q{1^{st}}_{F}O\right)\right)$$
15		fvex	$$⊢{\mathrm{Hom}}_{𝑓}\left(Q\right)\in \mathrm{V}$$
16	15	rnex	$$⊢\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\in \mathrm{V}$$
17		unexg	$$⊢\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\in \mathrm{V}\wedge U\in V\right)\to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\in \mathrm{V}$$
18	16 6 17	sylancr	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\in \mathrm{V}$$
19		ssidd	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\subseteq \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U$$
20		eqid	$$⊢\left(f\in \left(O\mathrm{Func}S\right),x\in {\mathrm{Base}}_C⟼\left(a\in \left(1^{st}\left(Y\right)\left(x\right)\left(O\mathrm{Nat}S\right)f\right)⟼a\left(x\right)\left(\mathrm{Id}\left(C\right)\left(x\right)\right)\right)\right)=\left(f\in \left(O\mathrm{Func}S\right),x\in {\mathrm{Base}}_C⟼\left(a\in \left(1^{st}\left(Y\right)\left(x\right)\left(O\mathrm{Nat}S\right)f\right)⟼a\left(x\right)\left(\mathrm{Id}\left(C\right)\left(x\right)\right)\right)\right)$$
21		eqid	$$⊢\mathrm{Inv}\left(\left(Q{\times }_{c}O\right)\mathrm{FuncCat}\mathrm{SetCat}\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\right)\right)=\mathrm{Inv}\left(\left(Q{\times }_{c}O\right)\mathrm{FuncCat}\mathrm{SetCat}\left(\mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\right)\right)$$
22		eqid	$$⊢\left(f\in \left(O\mathrm{Func}S\right),x\in {\mathrm{Base}}_C⟼\left(u\in 1^{st}\left(f\right)\left(x\right)⟼\left(y\in {\mathrm{Base}}_C⟼\left(g\in \left(y\mathrm{Hom}\left(C\right)x\right)⟼\left(x{2}^{nd}\left(f\right)y\right)\left(g\right)\left(u\right)\right)\right)\right)\right)=\left(f\in \left(O\mathrm{Func}S\right),x\in {\mathrm{Base}}_C⟼\left(u\in 1^{st}\left(f\right)\left(x\right)⟼\left(y\in {\mathrm{Base}}_C⟼\left(g\in \left(y\mathrm{Hom}\left(C\right)x\right)⟼\left(x{2}^{nd}\left(f\right)y\right)\left(g\right)\left(u\right)\right)\right)\right)\right)$$
23	1 8 9 2 3 10 4 11 12 13 14 5 18 7 19 20 21 22	yonffthlem	$$⊢\phi \to Y\in \left(\left(C\mathrm{Full}Q\right)\cap \left(C\mathrm{Faith}Q\right)\right)$$