Metamath Proof Explorer

Theorem yonpropd

Description: If two categories have the same set of objects, morphisms, and compositions, then they have the same Yoneda functor. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses hofpropd.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
hofpropd.2 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
hofpropd.c ⊢ φ → C ∈ Cat
hofpropd.d ⊢ φ → D ∈ Cat
Assertion yonpropd ⊢ φ → Yon ⁡ C = Yon ⁡ D

Proof

Step Hyp Ref Expression
1 hofpropd.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
2 hofpropd.2 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
3 hofpropd.c ⊢ φ → C ∈ Cat
4 hofpropd.d ⊢ φ → D ∈ Cat
5 1 oppchomfpropd ⊢ φ → Hom 𝑓 ⁡ oppCat ⁡ C = Hom 𝑓 ⁡ oppCat ⁡ D
6 1 2 oppccomfpropd ⊢ φ → comp 𝑓 ⁡ oppCat ⁡ C = comp 𝑓 ⁡ oppCat ⁡ D
7 eqid ⊢ oppCat ⁡ C = oppCat ⁡ C
8 7 oppccat ⊢ C ∈ Cat → oppCat ⁡ C ∈ Cat
9 3 8 syl ⊢ φ → oppCat ⁡ C ∈ Cat
10 eqid ⊢ oppCat ⁡ D = oppCat ⁡ D
11 10 oppccat ⊢ D ∈ Cat → oppCat ⁡ D ∈ Cat
12 4 11 syl ⊢ φ → oppCat ⁡ D ∈ Cat
13 eqid ⊢ Hom F ⁡ oppCat ⁡ C = Hom F ⁡ oppCat ⁡ C
14 eqid ⊢ SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C = SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C
15 fvex ⊢ Hom 𝑓 ⁡ C ∈ V
16 15 rnex ⊢ ran ⁡ Hom 𝑓 ⁡ C ∈ V
17 16 a1i ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ∈ V
18 ssidd ⊢ φ → ran ⁡ Hom 𝑓 ⁡ C ⊆ ran ⁡ Hom 𝑓 ⁡ C
19 7 13 14 3 17 18 oppchofcl ⊢ φ → Hom F ⁡ oppCat ⁡ C ∈ C × c oppCat ⁡ C Func SetCat ⁡ ran ⁡ Hom 𝑓 ⁡ C
20 1 2 5 6 3 4 9 12 19 curfpropd ⊢ φ → C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C = D oppCat ⁡ D curry F Hom F ⁡ oppCat ⁡ C
21 5 6 9 12 hofpropd ⊢ φ → Hom F ⁡ oppCat ⁡ C = Hom F ⁡ oppCat ⁡ D
22 21 oveq2d ⊢ φ → D oppCat ⁡ D curry F Hom F ⁡ oppCat ⁡ C = D oppCat ⁡ D curry F Hom F ⁡ oppCat ⁡ D
23 20 22 eqtrd ⊢ φ → C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C = D oppCat ⁡ D curry F Hom F ⁡ oppCat ⁡ D
24 eqid ⊢ Yon ⁡ C = Yon ⁡ C
25 24 3 7 13 yonval ⊢ φ → Yon ⁡ C = C oppCat ⁡ C curry F Hom F ⁡ oppCat ⁡ C
26 eqid ⊢ Yon ⁡ D = Yon ⁡ D
27 eqid ⊢ Hom F ⁡ oppCat ⁡ D = Hom F ⁡ oppCat ⁡ D
28 26 4 10 27 yonval ⊢ φ → Yon ⁡ D = D oppCat ⁡ D curry F Hom F ⁡ oppCat ⁡ D
29 23 25 28 3eqtr4d ⊢ φ → Yon ⁡ C = Yon ⁡ D