Theorem oyon1cl

Description: The opposite Yoneda embedding at an object of C is a functor from C to Set, also known as the covariant Hom functor. (Contributed by Mario Carneiro, 17-Jan-2017)

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

Proof

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