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 ⊢ φ → C ∈ Cat
yonval.o ⊢ O = oppCat ⁡ C
yoncl.s ⊢ S = SetCat ⁡ U
yoncl.q ⊢ Q = O FuncCat S
yoncl.u ⊢ φ → U ∈ V
yoncl.h ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ U
Assertion yoncl ⊢ φ → Y ∈ C Func Q

Proof

Step Hyp Ref Expression
1 yonval.y ⊢ Y = Yon ⁡ C
2 yonval.c ⊢ φ → C ∈ Cat
3 yonval.o ⊢ O = oppCat ⁡ C
4 yoncl.s ⊢ S = SetCat ⁡ U
5 yoncl.q ⊢ Q = O FuncCat S
6 yoncl.u ⊢ φ → U ∈ V
7 yoncl.h ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ U
8 eqid ⊢ Hom F ⁡ O = Hom F ⁡ O
9 1 2 3 8 yonval ⊢ φ → 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 ∈ Cat → O ∈ Cat
12 2 11 syl ⊢ φ → O ∈ Cat
13 3 8 4 2 6 7 oppchofcl ⊢ φ → Hom F ⁡ O ∈ C × c O Func S
14 10 5 2 12 13 curfcl ⊢ φ → C O curry F Hom F ⁡ O ∈ C Func Q
15 9 14 eqeltrd ⊢ φ → Y ∈ C Func Q