Metamath Proof Explorer

Theorem yon12

Description: Value of the Yoneda embedding at a morphism. 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
yon12.x ⊢ · ˙ = comp ⁡ C
yon12.w ⊢ φ → W ∈ B
yon12.f ⊢ φ → F ∈ W H Z
yon12.g ⊢ φ → G ∈ Z H X
Assertion yon12 ⊢ φ → Z 2 nd ⁡ 1 st ⁡ Y ⁡ X W ⁡ F ⁡ G = G W Z · ˙ X F

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 yon12.x ⊢ · ˙ = comp ⁡ C
8 yon12.w ⊢ φ → W ∈ B
9 yon12.f ⊢ φ → F ∈ W H Z
10 yon12.g ⊢ φ → G ∈ Z H X
11 eqid ⊢ oppCat ⁡ C = oppCat ⁡ C
12 eqid ⊢ Hom F ⁡ oppCat ⁡ C = Hom F ⁡ oppCat ⁡ C
13 1 3 11 12 yonval ⊢ φ → Y = C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C
14 13 fveq2d ⊢ φ → 1 st ⁡ Y = 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C
15 14 fveq1d ⊢ φ → 1 st ⁡ Y ⁡ X = 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X
16 15 fveq2d ⊢ φ → 2 nd ⁡ 1 st ⁡ Y ⁡ X = 2 nd ⁡ 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X
17 16 oveqd ⊢ φ → Z 2 nd ⁡ 1 st ⁡ Y ⁡ X W = Z 2 nd ⁡ 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X W
18 17 fveq1d ⊢ φ → Z 2 nd ⁡ 1 st ⁡ Y ⁡ X W ⁡ F = Z 2 nd ⁡ 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X W ⁡ F
19 eqid ⊢ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C = C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C
20 11 oppccat ⊢ C ∈ Cat → oppCat ⁡ C ∈ Cat
21 3 20 syl ⊢ φ → oppCat ⁡ C ∈ Cat
22 eqid ⊢ SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C = SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C
23 fvex ⊢ Hom 𝑓 ⁡ C ∈ V
24 23 rnex ⊢ ran ⁡ Hom 𝑓 ⁡ C ∈ V
25 24 a1i ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ∈ V
26 ssidd ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ ran ⁡ Hom 𝑓 ⁡ C
27 11 12 22 3 25 26 oppchofcl ⊢ φ → Hom F ⁡ oppCat ⁡ C ∈ C × c oppCat ⁡ C Func SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C
28 11 2 oppcbas ⊢ B = Base oppCat ⁡ C
29 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
30 eqid ⊢ Hom ⁡ oppCat ⁡ C = Hom ⁡ oppCat ⁡ C
31 eqid ⊢ Id ⁡ C = Id ⁡ C
32 5 11 oppchom ⊢ Z Hom ⁡ oppCat ⁡ C W = W H Z
33 9 32 eleqtrrdi ⊢ φ → F ∈ Z Hom ⁡ oppCat ⁡ C W
34 19 2 3 21 27 28 4 29 6 30 31 8 33 curf12 ⊢ φ → Z 2 nd ⁡ 1 st ⁡ C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C ⁡ X W ⁡ F = Id ⁡ C ⁡ X X Z 2 nd ⁡ Hom F ⁡ oppCat ⁡ C X W F
35 18 34 eqtrd ⊢ φ → Z 2 nd ⁡ 1 st ⁡ Y ⁡ X W ⁡ F = Id ⁡ C ⁡ X X Z 2 nd ⁡ Hom F ⁡ oppCat ⁡ C X W F
36 35 fveq1d ⊢ φ → Z 2 nd ⁡ 1 st ⁡ Y ⁡ X W ⁡ F ⁡ G = Id ⁡ C ⁡ X X Z 2 nd ⁡ Hom F ⁡ oppCat ⁡ C X W F ⁡ G
37 eqid ⊢ comp ⁡ oppCat ⁡ C = comp ⁡ oppCat ⁡ C
38 2 5 31 3 4 catidcl ⊢ φ → Id ⁡ C ⁡ X ∈ X H X
39 5 11 oppchom ⊢ X Hom ⁡ oppCat ⁡ C X = X H X
40 38 39 eleqtrrdi ⊢ φ → Id ⁡ C ⁡ X ∈ X Hom ⁡ oppCat ⁡ C X
41 5 11 oppchom ⊢ X Hom ⁡ oppCat ⁡ C Z = Z H X
42 10 41 eleqtrrdi ⊢ φ → G ∈ X Hom ⁡ oppCat ⁡ C Z
43 12 21 28 30 4 6 4 8 37 40 33 42 hof2 ⊢ φ → Id ⁡ C ⁡ X X Z 2 nd ⁡ Hom F ⁡ oppCat ⁡ C X W F ⁡ G = F X Z comp ⁡ oppCat ⁡ C W G X X comp ⁡ oppCat ⁡ C W Id ⁡ C ⁡ X
44 2 7 11 4 6 8 oppcco ⊢ φ → F X Z comp ⁡ oppCat ⁡ C W G = G W Z · ˙ X F
45 44 oveq1d ⊢ φ → F X Z comp ⁡ oppCat ⁡ C W G X X comp ⁡ oppCat ⁡ C W Id ⁡ C ⁡ X = G W Z · ˙ X F X X comp ⁡ oppCat ⁡ C W Id ⁡ C ⁡ X
46 2 7 11 4 4 8 oppcco ⊢ φ → G W Z · ˙ X F X X comp ⁡ oppCat ⁡ C W Id ⁡ C ⁡ X = Id ⁡ C ⁡ X W X · ˙ X G W Z · ˙ X F
47 2 5 7 3 8 6 4 9 10 catcocl ⊢ φ → G W Z · ˙ X F ∈ W H X
48 2 5 31 3 8 7 4 47 catlid ⊢ φ → Id ⁡ C ⁡ X W X · ˙ X G W Z · ˙ X F = G W Z · ˙ X F
49 45 46 48 3eqtrd ⊢ φ → F X Z comp ⁡ oppCat ⁡ C W G X X comp ⁡ oppCat ⁡ C W Id ⁡ C ⁡ X = G W Z · ˙ X F
50 36 43 49 3eqtrd ⊢ φ → Z 2 nd ⁡ 1 st ⁡ Y ⁡ X W ⁡ F ⁡ G = G W Z · ˙ X F