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	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yon11.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	yon11.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yon11.p	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	yon1cl.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	yon1cl.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	yon1cl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	yon1cl.h	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
Assertion	yon1cl	⊢ ( 𝜑 → ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		yon11.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yon11.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		yon11.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		yon11.p	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		yon1cl.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
6		yon1cl.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
7		yon1cl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
8		yon1cl.h	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
9		eqid	⊢ ( 𝑂 FuncCat 𝑆 ) = ( 𝑂 FuncCat 𝑆 )
10	9	fucbas	⊢ ( 𝑂 Func 𝑆 ) = ( Base ‘ ( 𝑂 FuncCat 𝑆 ) )
11		relfunc	⊢ Rel ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) )
12	1 3 5 6 9 7 8	yoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) )
13		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ∧ 𝑌 ∈ ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ) → ( 1st ‘ 𝑌 ) ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ( 2nd ‘ 𝑌 ) )
14	11 12 13	sylancr	⊢ ( 𝜑 → ( 1st ‘ 𝑌 ) ( 𝐶 Func ( 𝑂 FuncCat 𝑆 ) ) ( 2nd ‘ 𝑌 ) )
15	2 10 14	funcf1	⊢ ( 𝜑 → ( 1st ‘ 𝑌 ) : 𝐵 ⟶ ( 𝑂 Func 𝑆 ) )
16	15 4	ffvelcdmd	⊢ ( 𝜑 → ( ( 1st ‘ 𝑌 ) ‘ 𝑋 ) ∈ ( 𝑂 Func 𝑆 ) )