Metamath Proof Explorer

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	$⊢ φ \to C \in Cat$
		yon11.p	$⊢ φ \to X \in B$
		yon1cl.o	$⊢ O = oppCat (C)$
		yon1cl.s	$⊢ S = SetCat (U)$
		yon1cl.u	$⊢ φ \to U \in V$
		yon1cl.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq U$
	Assertion	yon1cl	$⊢ φ \to 1^{st} (Y) (X) \in (O Func S)$

Proof

Step	Hyp	Ref	Expression
1		yon11.y	$⊢ Y = Yon (C)$
2		yon11.b	$⊢ B = {Base}_{C}$
3		yon11.c	$⊢ φ \to C \in Cat$
4		yon11.p	$⊢ φ \to X \in B$
5		yon1cl.o	$⊢ O = oppCat (C)$
6		yon1cl.s	$⊢ S = SetCat (U)$
7		yon1cl.u	$⊢ φ \to U \in V$
8		yon1cl.h	$⊢ φ \to ran {Hom}_{𝑓} (C) \subseteq 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	$⊢ φ \to Y \in (C Func (O FuncCat S))$
13		1st2ndbr	$⊢ (Rel (C Func (O FuncCat S)) \land Y \in (C Func (O FuncCat S))) \to 1^{st} (Y) (C Func (O FuncCat S)) 2^{nd} (Y)$
14	11 12 13	sylancr	$⊢ φ \to 1^{st} (Y) (C Func (O FuncCat S)) 2^{nd} (Y)$
15	2 10 14	funcf1	$⊢ φ \to 1^{st} (Y) : B ⟶ O Func S$
16	15 4	ffvelrnd	$⊢ φ \to 1^{st} (Y) (X) \in (O Func S)$