Metamath Proof Explorer

Theorem yon11

Description: Value of the Yoneda embedding at an object. The partially evaluated Yoneda embedding is also 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 ⊢ φ → C ∈ Cat
yon11.p ⊢ φ → X ∈ B
yon11.h ⊢ H = Hom ⁡ C
yon11.z ⊢ φ → Z ∈ B
Assertion yon11 ⊢ φ → 1 st ⁡ 1 st ⁡ Y ⁡ X ⁡ Z = Z H X

Proof

Step Hyp Ref Expression
1 yon11.y ⊢ Y = Yon ⁡ C
2 yon11.b ⊢ B = Base C
3 yon11.c ⊢ φ → C ∈ Cat
4 yon11.p ⊢ φ → X ∈ B
5 yon11.h ⊢ H = Hom ⁡ C
6 yon11.z ⊢ φ → Z ∈ B
7 eqid ⊢ oppCat ⁡ C = oppCat ⁡ C
8 eqid ⊢ Hom F ⁡ oppCat ⁡ C = Hom F ⁡ oppCat ⁡ C
9 1 3 7 8 yonval ⊢ φ → Y = C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C
10 9 fveq2d ⊢ φ → 1 st ⁡ Y = 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C
11 10 fveq1d ⊢ φ → 1 st ⁡ Y ⁡ X = 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X
12 11 fveq2d ⊢ φ → 1 st ⁡ 1 st ⁡ Y ⁡ X = 1 st ⁡ 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X
13 12 fveq1d ⊢ φ → 1 st ⁡ 1 st ⁡ Y ⁡ X ⁡ Z = 1 st ⁡ 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X ⁡ Z
14 eqid ⊢ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C = C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C
15 7 oppccat ⊢ C ∈ Cat → oppCat ⁡ C ∈ Cat
16 3 15 syl ⊢ φ → oppCat ⁡ C ∈ Cat
17 eqid ⊢ SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C = SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C
18 fvex ⊢ Hom 𝑓 ⁡ C ∈ V
19 18 rnex ⊢ ran ⁡ Hom 𝑓 ⁡ C ∈ V
20 19 a1i ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ∈ V
21 ssidd ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ ran ⁡ Hom 𝑓 ⁡ C
22 7 8 17 3 20 21 oppchofcl ⊢ φ → Hom F ⁡ oppCat ⁡ C ∈ C × c oppCat ⁡ C Func SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C
23 7 2 oppcbas ⊢ B = Base oppCat ⁡ C
24 eqid ⊢ 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X = 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X
25 14 2 3 16 22 23 4 24 6 curf11 ⊢ φ → 1 st ⁡ 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X ⁡ Z = X 1 st ⁡ Hom F ⁡ oppCat ⁡ C Z
26 eqid ⊢ Hom ⁡ oppCat ⁡ C = Hom ⁡ oppCat ⁡ C
27 8 16 23 26 4 6 hof1 ⊢ φ → X 1 st ⁡ Hom F ⁡ oppCat ⁡ C Z = X Hom ⁡ oppCat ⁡ C Z
28 5 7 oppchom ⊢ X Hom ⁡ oppCat ⁡ C Z = Z H X
29 27 28 eqtrdi ⊢ φ → X 1 st ⁡ Hom F ⁡ oppCat ⁡ C Z = Z H X
30 13 25 29 3eqtrd ⊢ φ → 1 st ⁡ 1 st ⁡ Y ⁡ X ⁡ Z = Z H X