df-yon

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

		Ref	Expression
	Assertion	df-yon	$⊢ Yon = (c \in Cat ⟼ ⟨c, oppCat (c)⟩ {curry}_{F} {Hom}_{F} (oppCat (c)))$

Step	Hyp	Ref	Expression
0		cyon	$class Yon$
1		vc	$setvar c$
2		ccat	$class Cat$
3	1	cv	$setvar c$
4		coppc	$class oppCat$
5	3 4	cfv	$class oppCat (c)$
6	3 5	cop	$class ⟨c, oppCat (c)⟩$
7		ccurf	$class {curry}_{F}$
8		chof	$class {Hom}_{F}$
9	5 8	cfv	$class {Hom}_{F} (oppCat (c))$
10	6 9 7	co	$class (⟨c, oppCat (c)⟩ {curry}_{F} {Hom}_{F} (oppCat (c)))$
11	1 2 10	cmpt	$class (c \in Cat ⟼ ⟨c, oppCat (c)⟩ {curry}_{F} {Hom}_{F} (oppCat (c)))$
12	0 11	wceq	$wff Yon = (c \in Cat ⟼ ⟨c, oppCat (c)⟩ {curry}_{F} {Hom}_{F} (oppCat (c)))$

Metamath Proof Explorer