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=BaseC
yon11.c ⊢φ→C∈Cat
yon11.p ⊢φ→X∈B
yon11.h ⊢H=Hom⁡C
yon11.z ⊢φ→Z∈B
Assertion yon11 ⊢φ→1st⁡1st⁡Y⁡X⁡Z=ZHX

Proof

Step Hyp Ref Expression
1 yon11.y ⊢Y=Yon⁡C
2 yon11.b ⊢B=BaseC
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 ⊢HomF⁡oppCat⁡C=HomF⁡oppCat⁡C
9 1 3 7 8 yonval ⊢φ→Y=CoppCat⁡CcurryFHomF⁡oppCat⁡C
10 9 fveq2d ⊢φ→1st⁡Y=1st⁡CoppCat⁡CcurryFHomF⁡oppCat⁡C
11 10 fveq1d ⊢φ→1st⁡Y⁡X=1st⁡CoppCat⁡CcurryFHomF⁡oppCat⁡C⁡X
12 11 fveq2d ⊢φ→1st⁡1st⁡Y⁡X=1st⁡1st⁡CoppCat⁡CcurryFHomF⁡oppCat⁡C⁡X
13 12 fveq1d ⊢φ→1st⁡1st⁡Y⁡X⁡Z=1st⁡1st⁡CoppCat⁡CcurryFHomF⁡oppCat⁡C⁡X⁡Z
14 eqid ⊢CoppCat⁡CcurryFHomF⁡oppCat⁡C=CoppCat⁡CcurryFHomF⁡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 ⊢φ→HomF⁡oppCat⁡C∈C×coppCat⁡CFuncSetCat⁡ran⁡Hom𝑓⁡C
23 7 2 oppcbas ⊢B=BaseoppCat⁡C
24 eqid ⊢1st⁡CoppCat⁡CcurryFHomF⁡oppCat⁡C⁡X=1st⁡CoppCat⁡CcurryFHomF⁡oppCat⁡C⁡X
25 14 2 3 16 22 23 4 24 6 curf11 ⊢φ→1st⁡1st⁡CoppCat⁡CcurryFHomF⁡oppCat⁡C⁡X⁡Z=X1st⁡HomF⁡oppCat⁡CZ
26 eqid ⊢Hom⁡oppCat⁡C=Hom⁡oppCat⁡C
27 8 16 23 26 4 6 hof1 ⊢φ→X1st⁡HomF⁡oppCat⁡CZ=XHom⁡oppCat⁡CZ
28 5 7 oppchom ⊢XHom⁡oppCat⁡CZ=ZHX
29 27 28 eqtrdi ⊢φ→X1st⁡HomF⁡oppCat⁡CZ=ZHX
30 13 25 29 3eqtrd ⊢φ→1st⁡1st⁡Y⁡X⁡Z=ZHX