Definition df-yon 16891

Description: Define the Yoneda embedding, which is the currying of the (opposite) Hom functor. (Contributed by Mario Carneiro, 11-Jan-2017.)

Assertion

Ref	Expression
df-yon	|- Yon = ( c e. Cat |-> ( <. c , (oppCat ` c ) >. curryF (HomF ` (oppCat ` c ) ) ) )

Detailed syntax breakdown of Definition df-yon

Step	Hyp	Ref	Expression
1		cyon 16889	. 2 class Yon
2		vc	. . 3 setvar c
3		ccat 16325	. . 3 class Cat
4	2	cv 1482	. . . . 5 class c
5		coppc 16371	. . . . . 6 class oppCat
6	4, 5	cfv 5888	. . . . 5 class (oppCat ` c )
7	4, 6	cop 4183	. . . 4 class <. c , (oppCat ` c ) >.
8		chof 16888	. . . . 5 class HomF
9	6, 8	cfv 5888	. . . 4 class (HomF ` (oppCat ` c ) )
10		ccurf 16850	. . . 4 class curryF
11	7, 9, 10	co 6650	. . 3 class ( <. c , (oppCat ` c ) >. curryF (HomF ` (oppCat ` c ) ) )
12	2, 3, 11	cmpt 4729	. 2 class ( c e. Cat |-> ( <. c , (oppCat ` c ) >. curryF (HomF ` (oppCat ` c ) ) ) )
13	1, 12	wceq 1483	1 wff Yon = ( c e. Cat |-> ( <. c , (oppCat ` c ) >. curryF (HomF ` (oppCat ` c ) ) ) )

This definition is referenced by:  yonval  16901