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 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
hofpropd.2 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
hofpropd.c 
|- ( ph -> C e. Cat )
hofpropd.d 
|- ( ph -> D e. Cat )
Assertion yonpropd 
|- ( ph -> ( Yon ` C ) = ( Yon ` D ) )

Proof

Step Hyp Ref Expression
1 hofpropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 hofpropd.2 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 hofpropd.c 
 |-  ( ph -> C e. Cat )
4 hofpropd.d 
 |-  ( ph -> D e. Cat )
5 1 oppchomfpropd 
 |-  ( ph -> ( Homf ` ( oppCat ` C ) ) = ( Homf ` ( oppCat ` D ) ) )
6 1 2 oppccomfpropd 
 |-  ( ph -> ( comf ` ( oppCat ` C ) ) = ( comf ` ( oppCat ` D ) ) )
7 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
8 7 oppccat 
 |-  ( C e. Cat -> ( oppCat ` C ) e. Cat )
9 3 8 syl 
 |-  ( ph -> ( oppCat ` C ) e. Cat )
10 eqid 
 |-  ( oppCat ` D ) = ( oppCat ` D )
11 10 oppccat 
 |-  ( D e. Cat -> ( oppCat ` D ) e. Cat )
12 4 11 syl 
 |-  ( ph -> ( oppCat ` D ) e. Cat )
13 eqid 
 |-  ( HomF ` ( oppCat ` C ) ) = ( HomF ` ( oppCat ` C ) )
14 eqid 
 |-  ( SetCat ` ran ( Homf ` C ) ) = ( SetCat ` ran ( Homf ` C ) )
15 fvex 
 |-  ( Homf ` C ) e. _V
16 15 rnex 
 |-  ran ( Homf ` C ) e. _V
17 16 a1i 
 |-  ( ph -> ran ( Homf ` C ) e. _V )
18 ssidd 
 |-  ( ph -> ran ( Homf ` C ) C_ ran ( Homf ` C ) )
19 7 13 14 3 17 18 oppchofcl 
 |-  ( ph -> ( HomF ` ( oppCat ` C ) ) e. ( ( C Xc. ( oppCat ` C ) ) Func ( SetCat ` ran ( Homf ` C ) ) ) )
20 1 2 5 6 3 4 9 12 19 curfpropd 
 |-  ( ph -> ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) = ( <. D , ( oppCat ` D ) >. curryF ( HomF ` ( oppCat ` C ) ) ) )
21 5 6 9 12 hofpropd 
 |-  ( ph -> ( HomF ` ( oppCat ` C ) ) = ( HomF ` ( oppCat ` D ) ) )
22 21 oveq2d 
 |-  ( ph -> ( <. D , ( oppCat ` D ) >. curryF ( HomF ` ( oppCat ` C ) ) ) = ( <. D , ( oppCat ` D ) >. curryF ( HomF ` ( oppCat ` D ) ) ) )
23 20 22 eqtrd 
 |-  ( ph -> ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) = ( <. D , ( oppCat ` D ) >. curryF ( HomF ` ( oppCat ` D ) ) ) )
24 eqid 
 |-  ( Yon ` C ) = ( Yon ` C )
25 24 3 7 13 yonval 
 |-  ( ph -> ( Yon ` C ) = ( <. C , ( oppCat ` C ) >. curryF ( HomF ` ( oppCat ` C ) ) ) )
26 eqid 
 |-  ( Yon ` D ) = ( Yon ` D )
27 eqid 
 |-  ( HomF ` ( oppCat ` D ) ) = ( HomF ` ( oppCat ` D ) )
28 26 4 10 27 yonval 
 |-  ( ph -> ( Yon ` D ) = ( <. D , ( oppCat ` D ) >. curryF ( HomF ` ( oppCat ` D ) ) ) )
29 23 25 28 3eqtr4d 
 |-  ( ph -> ( Yon ` C ) = ( Yon ` D ) )