Theorem yoneda

Description: The Yoneda Lemma. There is a natural isomorphism between the functors Z and E , where Z ( F , X ) is the natural transformations from Yon ( X ) = Hom ( - , X ) to F , and E ( F , X ) = F ( X ) is the evaluation functor. Here we need two universes to state the claim: the smaller universe U is used for forming the functor category Q = C ^op -> SetCat ( U ) , which itself does not (necessarily) live in U but instead is an element of the larger universe V . (If U is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set U = V in this case.) (Contributed by Mario Carneiro, 29-Jan-2017)

	Ref	Expression
Hypotheses	yoneda.y	$$⊢Y=\mathrm{Yon}\left(C\right)$$
	yoneda.b	$$⊢B={\mathrm{Base}}_C$$
	yoneda.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	yoneda.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	yoneda.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
	yoneda.t	$$⊢T=\mathrm{SetCat}\left(V\right)$$
	yoneda.q	$$⊢Q=O\mathrm{FuncCat}S$$
	yoneda.h	$$⊢H={Hom}_F\left(Q\right)$$
	yoneda.r	$$⊢R=\left(Q{\times }_{c}O\right)\mathrm{FuncCat}T$$
	yoneda.e	$$⊢E=O{eval}_{F}S$$
	yoneda.z	$$⊢Z=H{\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)$$
	yoneda.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	yoneda.w	$$⊢\phi \to V\in W$$
	yoneda.u	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\subseteq U$$
	yoneda.v	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\subseteq V$$
	yoneda.m	$$⊢M=\left(f\in \left(O\mathrm{Func}S\right),x\in B⟼\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(\underset{\dot{}}{1}\left(x\right)\right)\right)\right)$$
	yoneda.i	$$⊢I=\mathrm{Iso}\left(R\right)$$
Assertion	yoneda	$$⊢\phi \to M\in \left(ZIE\right)$$

Proof

Step	Hyp	Ref	Expression
1		yoneda.y	$$⊢Y=\mathrm{Yon}\left(C\right)$$
2		yoneda.b	$$⊢B={\mathrm{Base}}_C$$
3		yoneda.1	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
4		yoneda.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
5		yoneda.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
6		yoneda.t	$$⊢T=\mathrm{SetCat}\left(V\right)$$
7		yoneda.q	$$⊢Q=O\mathrm{FuncCat}S$$
8		yoneda.h	$$⊢H={Hom}_F\left(Q\right)$$
9		yoneda.r	$$⊢R=\left(Q{\times }_{c}O\right)\mathrm{FuncCat}T$$
10		yoneda.e	$$⊢E=O{eval}_{F}S$$
11		yoneda.z	$$⊢Z=H{\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)$$
12		yoneda.c	$$⊢\phi \to C\in \mathrm{Cat}$$
13		yoneda.w	$$⊢\phi \to V\in W$$
14		yoneda.u	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(C\right)\subseteq U$$
15		yoneda.v	$$⊢\phi \to \mathrm{ran}{\mathrm{Hom}}_{𝑓}\left(Q\right)\cup U\subseteq V$$
16		yoneda.m	$$⊢M=\left(f\in \left(O\mathrm{Func}S\right),x\in B⟼\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(\underset{\dot{}}{1}\left(x\right)\right)\right)\right)$$
17		yoneda.i	$$⊢I=\mathrm{Iso}\left(R\right)$$
18	9	fucbas	$$⊢\left(Q{\times }_{c}O\right)\mathrm{Func}T={\mathrm{Base}}_R$$
19		eqid	$$⊢\mathrm{Inv}\left(R\right)=\mathrm{Inv}\left(R\right)$$
20	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	yonedalem1	$$⊢\phi \to \left(Z\in \left(\left(Q{\times }_{c}O\right)\mathrm{Func}T\right)\wedge E\in \left(\left(Q{\times }_{c}O\right)\mathrm{Func}T\right)\right)$$
21	20	simpld	$$⊢\phi \to Z\in \left(\left(Q{\times }_{c}O\right)\mathrm{Func}T\right)$$
22		funcrcl	$$⊢Z\in \left(\left(Q{\times }_{c}O\right)\mathrm{Func}T\right)\to \left(Q{\times }_{c}O\in \mathrm{Cat}\wedge T\in \mathrm{Cat}\right)$$
23	21 22	syl	$$⊢\phi \to \left(Q{\times }_{c}O\in \mathrm{Cat}\wedge T\in \mathrm{Cat}\right)$$
24	23	simpld	$$⊢\phi \to Q{\times }_{c}O\in \mathrm{Cat}$$
25	23	simprd	$$⊢\phi \to T\in \mathrm{Cat}$$
26	9 24 25	fuccat	$$⊢\phi \to R\in \mathrm{Cat}$$
27	20	simprd	$$⊢\phi \to E\in \left(\left(Q{\times }_{c}O\right)\mathrm{Func}T\right)$$
28		eqid	$$⊢\left(f\in \left(O\mathrm{Func}S\right),x\in B⟼\left(u\in 1^{st}\left(f\right)\left(x\right)⟼\left(y\in B⟼\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 B⟼\left(u\in 1^{st}\left(f\right)\left(x\right)⟼\left(y\in B⟼\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)$$
29	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 19 28	yonedainv	$$⊢\phi \to M\left(Z\mathrm{Inv}\left(R\right)E\right)\left(f\in \left(O\mathrm{Func}S\right),x\in B⟼\left(u\in 1^{st}\left(f\right)\left(x\right)⟼\left(y\in B⟼\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)$$
30	18 19 26 21 27 17 29	inviso1	$$⊢\phi \to M\in \left(ZIE\right)$$