Metamath Proof Explorer

Theorem oppcyon

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

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

Proof

Step Hyp Ref Expression
1 oppcyon.o ⊢ O = oppCat ⁡ C
2 oppcyon.y ⊢ Y = Yon ⁡ O
3 oppcyon.m ⊢ M = Hom F ⁡ C
4 oppcyon.c ⊢ φ → C ∈ Cat
5 1 2oppchomf ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
6 5 a1i ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ O
7 1 2oppccomf ⊢ comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
8 7 a1i ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ oppCat ⁡ O
9 1 oppccat ⊢ C ∈ Cat → O ∈ Cat
10 4 9 syl ⊢ φ → O ∈ Cat
11 eqid ⊢ oppCat ⁡ O = oppCat ⁡ O
12 11 oppccat ⊢ O ∈ Cat → oppCat ⁡ O ∈ Cat
13 10 12 syl ⊢ φ → oppCat ⁡ O ∈ Cat
14 6 8 4 13 hofpropd ⊢ φ → Hom F ⁡ C = Hom F ⁡ oppCat ⁡ O
15 3 14 eqtrid ⊢ φ → M = Hom F ⁡ oppCat ⁡ O
16 15 oveq2d ⊢ φ → O oppCat ⁡ O curry F M = O oppCat ⁡ O curry F Hom F ⁡ oppCat ⁡ O
17 eqidd ⊢ φ → Hom 𝑓 ⁡ O = Hom 𝑓 ⁡ O
18 eqidd ⊢ φ → comp 𝑓 ⁡ O = comp 𝑓 ⁡ O
19 eqid ⊢ SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C = SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C
20 fvex ⊢ Hom 𝑓 ⁡ C ∈ V
21 20 rnex ⊢ ran ⁡ Hom 𝑓 ⁡ C ∈ V
22 21 a1i ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ∈ V
23 ssidd ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ ran ⁡ Hom 𝑓 ⁡ C
24 3 1 19 4 22 23 hofcl ⊢ φ → M ∈ O × c C Func SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C
25 17 18 6 8 10 10 4 13 24 curfpropd ⊢ φ → O C curry F M = O oppCat ⁡ O curry F M
26 eqid ⊢ Hom F ⁡ oppCat ⁡ O = Hom F ⁡ oppCat ⁡ O
27 2 10 11 26 yonval ⊢ φ → Y = O oppCat ⁡ O curry F Hom F ⁡ oppCat ⁡ O
28 16 25 27 3eqtr4rd ⊢ φ → Y = O C curry F M