Metamath Proof Explorer

Theorem yonval

Description: Value of the Yoneda embedding. (Contributed by Mario Carneiro, 17-Jan-2017)

Ref Expression
Hypotheses yonval.y ⊢ Y = Yon ⁡ C
yonval.c ⊢ φ → C ∈ Cat
yonval.o ⊢ O = oppCat ⁡ C
yonval.m ⊢ M = Hom F ⁡ O
Assertion yonval ⊢ φ → Y = C O curry F M

Proof

Step Hyp Ref Expression
1 yonval.y ⊢ Y = Yon ⁡ C
2 yonval.c ⊢ φ → C ∈ Cat
3 yonval.o ⊢ O = oppCat ⁡ C
4 yonval.m ⊢ M = Hom F ⁡ O
5 df-yon ⊢ Yon = c ∈ Cat ⟼ c oppCat ⁡ c curry F Hom F ⁡ oppCat ⁡ c
6 simpr ⊢ φ ∧ c = C → c = C
7 6 fveq2d ⊢ φ ∧ c = C → oppCat ⁡ c = oppCat ⁡ C
8 7 3 eqtr4di ⊢ φ ∧ c = C → oppCat ⁡ c = O
9 6 8 opeq12d ⊢ φ ∧ c = C → c oppCat ⁡ c = C O
10 8 fveq2d ⊢ φ ∧ c = C → Hom F ⁡ oppCat ⁡ c = Hom F ⁡ O
11 10 4 eqtr4di ⊢ φ ∧ c = C → Hom F ⁡ oppCat ⁡ c = M
12 9 11 oveq12d ⊢ φ ∧ c = C → c oppCat ⁡ c curry F Hom F ⁡ oppCat ⁡ c = C O curry F M
13 ovexd ⊢ φ → C O curry F M ∈ V
14 5 12 2 13 fvmptd2 ⊢ φ → Yon ⁡ C = C O curry F M
15 1 14 syl5eq ⊢ φ → Y = C O curry F M