Theorem yoncl

Description: The Yoneda embedding is a functor from the category to the category Q of presheaves on C . (Contributed by Mario Carneiro, 17-Jan-2017)

	Ref	Expression
Hypotheses	yonval.y	|- Y = ( Yon ` C )
	yonval.c	|- ( ph -> C e. Cat )
	yonval.o	|- O = ( oppCat ` C )
	yoncl.s	|- S = ( SetCat ` U )
	yoncl.q	|- Q = ( O FuncCat S )
	yoncl.u	|- ( ph -> U e. V )
	yoncl.h	|- ( ph -> ran ( Homf ` C ) C_ U )
Assertion	yoncl	|- ( ph -> Y e. ( C Func Q ) )

Proof

Step	Hyp	Ref	Expression
1		yonval.y	|- Y = ( Yon ` C )
2		yonval.c	|- ( ph -> C e. Cat )
3		yonval.o	|- O = ( oppCat ` C )
4		yoncl.s	|- S = ( SetCat ` U )
5		yoncl.q	|- Q = ( O FuncCat S )
6		yoncl.u	|- ( ph -> U e. V )
7		yoncl.h	|- ( ph -> ran ( Homf ` C ) C_ U )
8		eqid	|- ( HomF ` O ) = ( HomF ` O )
9	1 2 3 8	yonval	|- ( ph -> Y = ( <. C , O >. curryF ( HomF ` O ) ) )
10		eqid	|- ( <. C , O >. curryF ( HomF ` O ) ) = ( <. C , O >. curryF ( HomF ` O ) )
11	3	oppccat	|- ( C e. Cat -> O e. Cat )
12	2 11	syl	|- ( ph -> O e. Cat )
13	3 8 4 2 6 7	oppchofcl	|- ( ph -> ( HomF ` O ) e. ( ( C Xc. O ) Func S ) )
14	10 5 2 12 13	curfcl	|- ( ph -> ( <. C , O >. curryF ( HomF ` O ) ) e. ( C Func Q ) )
15	9 14	eqeltrd	|- ( ph -> Y e. ( C Func Q ) )