Theorem yon1cl

Description: The Yoneda embedding at an object of C is a presheaf on C , also known as the contravariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017)

	Ref	Expression
Hypotheses	yon11.y	|- Y = ( Yon ` C )
	yon11.b	|- B = ( Base ` C )
	yon11.c	|- ( ph -> C e. Cat )
	yon11.p	|- ( ph -> X e. B )
	yon1cl.o	|- O = ( oppCat ` C )
	yon1cl.s	|- S = ( SetCat ` U )
	yon1cl.u	|- ( ph -> U e. V )
	yon1cl.h	|- ( ph -> ran ( Homf ` C ) C_ U )
Assertion	yon1cl	|- ( ph -> ( ( 1st ` Y ) ` X ) e. ( O Func S ) )

Proof

Step	Hyp	Ref	Expression
1		yon11.y	|- Y = ( Yon ` C )
2		yon11.b	|- B = ( Base ` C )
3		yon11.c	|- ( ph -> C e. Cat )
4		yon11.p	|- ( ph -> X e. B )
5		yon1cl.o	|- O = ( oppCat ` C )
6		yon1cl.s	|- S = ( SetCat ` U )
7		yon1cl.u	|- ( ph -> U e. V )
8		yon1cl.h	|- ( ph -> ran ( Homf ` C ) C_ U )
9		eqid	|- ( O FuncCat S ) = ( O FuncCat S )
10	9	fucbas	|- ( O Func S ) = ( Base ` ( O FuncCat S ) )
11		relfunc	|- Rel ( C Func ( O FuncCat S ) )
12	1 3 5 6 9 7 8	yoncl	|- ( ph -> Y e. ( C Func ( O FuncCat S ) ) )
13		1st2ndbr	|- ( ( Rel ( C Func ( O FuncCat S ) ) /\ Y e. ( C Func ( O FuncCat S ) ) ) -> ( 1st ` Y ) ( C Func ( O FuncCat S ) ) ( 2nd ` Y ) )
14	11 12 13	sylancr	|- ( ph -> ( 1st ` Y ) ( C Func ( O FuncCat S ) ) ( 2nd ` Y ) )
15	2 10 14	funcf1	|- ( ph -> ( 1st ` Y ) : B --> ( O Func S ) )
16	15 4	ffvelrnd	|- ( ph -> ( ( 1st ` Y ) ` X ) e. ( O Func S ) )