Metamath Proof Explorer

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	$⊢ φ \to C \in Cat$
		yonval.o	$⊢ O = oppCat (C)$
		yoncl.s	$⊢ S = SetCat (U)$
		yoncl.q	$⊢ Q = O FuncCat S$
		yoncl.u	$⊢ φ \to U \in V$
		yoncl.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
	Assertion	yoncl	$⊢ φ \to Y \in (C Func Q)$

Proof

Step	Hyp	Ref	Expression
1		yonval.y	$⊢ Y = Yon (C)$
2		yonval.c	$⊢ φ \to C \in Cat$
3		yonval.o	$⊢ O = oppCat (C)$
4		yoncl.s	$⊢ S = SetCat (U)$
5		yoncl.q	$⊢ Q = O FuncCat S$
6		yoncl.u	$⊢ φ \to U \in V$
7		yoncl.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
8		eqid	$⊢ {Hom}_{F} (O) = {Hom}_{F} (O)$
9	1 2 3 8	yonval	$⊢ φ \to Y = ⟨C, O⟩ {curry}_{F} {Hom}_{F} (O)$
10		eqid	$⊢ ⟨C, O⟩ {curry}_{F} {Hom}_{F} (O) = ⟨C, O⟩ {curry}_{F} {Hom}_{F} (O)$
11	3	oppccat	$⊢ C \in Cat \to O \in Cat$
12	2 11	syl	$⊢ φ \to O \in Cat$
13	3 8 4 2 6 7	oppchofcl	$⊢ φ \to {Hom}_{F} (O) \in ((C \times_{c} O) Func S)$
14	10 5 2 12 13	curfcl	$⊢ φ \to ⟨C, O⟩ {curry}_{F} {Hom}_{F} (O) \in (C Func Q)$
15	9 14	eqeltrd	$⊢ φ \to Y \in (C Func Q)$