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 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
hofpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
hofpropd.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
hofpropd.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion yonpropd ( 𝜑 → ( Yon ‘ 𝐶 ) = ( Yon ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 hofpropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2 hofpropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3 hofpropd.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 hofpropd.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
5 1 oppchomfpropd ⊢ ( 𝜑 → ( Homf ‘ ( oppCat ‘ 𝐶 ) ) = ( Homf ‘ ( oppCat ‘ 𝐷 ) ) )
6 1 2 oppccomfpropd ⊢ ( 𝜑 → ( compf ‘ ( oppCat ‘ 𝐶 ) ) = ( compf ‘ ( oppCat ‘ 𝐷 ) ) )
7 eqid ⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
8 7 oppccat ⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat )
9 3 8 syl ⊢ ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat )
10 eqid ⊢ ( oppCat ‘ 𝐷 ) = ( oppCat ‘ 𝐷 )
11 10 oppccat ⊢ ( 𝐷 ∈ Cat → ( oppCat ‘ 𝐷 ) ∈ Cat )
12 4 11 syl ⊢ ( 𝜑 → ( oppCat ‘ 𝐷 ) ∈ Cat )
13 eqid ⊢ ( HomF ‘ ( oppCat ‘ 𝐶 ) ) = ( HomF ‘ ( oppCat ‘ 𝐶 ) )
14 eqid ⊢ ( SetCat ‘ ran ( Homf ‘ 𝐶 ) ) = ( SetCat ‘ ran ( Homf ‘ 𝐶 ) )
15 fvex ⊢ ( Homf ‘ 𝐶 ) ∈ V
16 15 rnex ⊢ ran ( Homf ‘ 𝐶 ) ∈ V
17 16 a1i ⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ∈ V )
18 ssidd ⊢ ( 𝜑 → ran ( Homf ‘ 𝐶 ) ⊆ ran ( Homf ‘ 𝐶 ) )
19 7 13 14 3 17 18 oppchofcl ⊢ ( 𝜑 → ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ∈ ( ( 𝐶 ×c ( oppCat ‘ 𝐶 ) ) Func ( SetCat ‘ ran ( Homf ‘ 𝐶 ) ) ) )
20 1 2 5 6 3 4 9 12 19 curfpropd ⊢ ( 𝜑 → ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) = ( ⟨ 𝐷 , ( oppCat ‘ 𝐷 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) )
21 5 6 9 12 hofpropd ⊢ ( 𝜑 → ( HomF ‘ ( oppCat ‘ 𝐶 ) ) = ( HomF ‘ ( oppCat ‘ 𝐷 ) ) )
22 21 oveq2d ⊢ ( 𝜑 → ( ⟨ 𝐷 , ( oppCat ‘ 𝐷 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) = ( ⟨ 𝐷 , ( oppCat ‘ 𝐷 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐷 ) ) ) )
23 20 22 eqtrd ⊢ ( 𝜑 → ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) = ( ⟨ 𝐷 , ( oppCat ‘ 𝐷 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐷 ) ) ) )
24 eqid ⊢ ( Yon ‘ 𝐶 ) = ( Yon ‘ 𝐶 )
25 24 3 7 13 yonval ⊢ ( 𝜑 → ( Yon ‘ 𝐶 ) = ( ⟨ 𝐶 , ( oppCat ‘ 𝐶 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐶 ) ) ) )
26 eqid ⊢ ( Yon ‘ 𝐷 ) = ( Yon ‘ 𝐷 )
27 eqid ⊢ ( HomF ‘ ( oppCat ‘ 𝐷 ) ) = ( HomF ‘ ( oppCat ‘ 𝐷 ) )
28 26 4 10 27 yonval ⊢ ( 𝜑 → ( Yon ‘ 𝐷 ) = ( ⟨ 𝐷 , ( oppCat ‘ 𝐷 ) ⟩ curryF ( HomF ‘ ( oppCat ‘ 𝐷 ) ) ) )
29 23 25 28 3eqtr4d ⊢ ( 𝜑 → ( Yon ‘ 𝐶 ) = ( Yon ‘ 𝐷 ) )