Metamath Proof Explorer

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

Proof

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