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	⊢ 𝑌 = ( Yon ‘ 𝐶 )
	yonval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	yonval.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	yoncl.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
	yoncl.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
	yoncl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
	yoncl.h	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
Assertion	yoncl	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		yonval.y	⊢ 𝑌 = ( Yon ‘ 𝐶 )
2		yonval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
3		yonval.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
4		yoncl.s	⊢ 𝑆 = ( SetCat ‘ 𝑈 )
5		yoncl.q	⊢ 𝑄 = ( 𝑂 FuncCat 𝑆 )
6		yoncl.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
7		yoncl.h	⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ 𝑈 )
8		eqid	⊢ ( HomF ‘ 𝑂 ) = ( HomF ‘ 𝑂 )
9	1 2 3 8	yonval	⊢ ( 𝜑 → 𝑌 = ( ⟨ 𝐶 , 𝑂 ⟩ curryF ( HomF ‘ 𝑂 ) ) )
10		eqid	⊢ ( ⟨ 𝐶 , 𝑂 ⟩ curryF ( HomF ‘ 𝑂 ) ) = ( ⟨ 𝐶 , 𝑂 ⟩ curryF ( HomF ‘ 𝑂 ) )
11	3	oppccat	⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
12	2 11	syl	⊢ ( 𝜑 → 𝑂 ∈ Cat )
13	3 8 4 2 6 7	oppchofcl	⊢ ( 𝜑 → ( HomF ‘ 𝑂 ) ∈ ( ( 𝐶 ×c 𝑂 ) Func 𝑆 ) )
14	10 5 2 12 13	curfcl	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝑂 ⟩ curryF ( HomF ‘ 𝑂 ) ) ∈ ( 𝐶 Func 𝑄 ) )
15	9 14	eqeltrd	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐶 Func 𝑄 ) )