Metamath Proof Explorer

Theorem oppccomfpropd

Description: If two categories have the same hom-sets and composition, so do their opposites. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses oppchomfpropd.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` D ) )
oppccomfpropd.1 
|- ( ph -> ( comf ` C ) = ( comf ` D ) )
Assertion oppccomfpropd 
|- ( ph -> ( comf ` ( oppCat ` C ) ) = ( comf ` ( oppCat ` D ) ) )

Proof

Step Hyp Ref Expression
1 oppchomfpropd.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` D ) )
2 oppccomfpropd.1 
 |-  ( ph -> ( comf ` C ) = ( comf ` D ) )
3 eqid 
 |-  ( Base ` C ) = ( Base ` C )
4 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
5 eqid 
 |-  ( comp ` C ) = ( comp ` C )
6 eqid 
 |-  ( comp ` D ) = ( comp ` D )
7 1 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> ( Homf ` C ) = ( Homf ` D ) )
8 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> ( comf ` C ) = ( comf ` D ) )
9 simplr3 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> z e. ( Base ` C ) )
10 simplr2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> y e. ( Base ` C ) )
11 simplr1 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> x e. ( Base ` C ) )
12 simprr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> g e. ( y ( Hom ` ( oppCat ` C ) ) z ) )
13 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
14 4 13 oppchom 
 |-  ( y ( Hom ` ( oppCat ` C ) ) z ) = ( z ( Hom ` C ) y )
15 12 14 eleqtrdi 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> g e. ( z ( Hom ` C ) y ) )
16 simprl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> f e. ( x ( Hom ` ( oppCat ` C ) ) y ) )
17 4 13 oppchom 
 |-  ( x ( Hom ` ( oppCat ` C ) ) y ) = ( y ( Hom ` C ) x )
18 16 17 eleqtrdi 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> f e. ( y ( Hom ` C ) x ) )
19 3 4 5 6 7 8 9 10 11 15 18 comfeqval 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> ( f ( <. z , y >. ( comp ` C ) x ) g ) = ( f ( <. z , y >. ( comp ` D ) x ) g ) )
20 3 5 13 11 10 9 oppcco 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> ( g ( <. x , y >. ( comp ` ( oppCat ` C ) ) z ) f ) = ( f ( <. z , y >. ( comp ` C ) x ) g ) )
21 eqid 
 |-  ( Base ` D ) = ( Base ` D )
22 eqid 
 |-  ( oppCat ` D ) = ( oppCat ` D )
23 1 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` D ) )
24 23 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> ( Base ` C ) = ( Base ` D ) )
25 11 24 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> x e. ( Base ` D ) )
26 10 24 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> y e. ( Base ` D ) )
27 9 24 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> z e. ( Base ` D ) )
28 21 6 22 25 26 27 oppcco 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> ( g ( <. x , y >. ( comp ` ( oppCat ` D ) ) z ) f ) = ( f ( <. z , y >. ( comp ` D ) x ) g ) )
29 19 20 28 3eqtr4d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` ( oppCat ` C ) ) y ) /\ g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ) ) -> ( g ( <. x , y >. ( comp ` ( oppCat ` C ) ) z ) f ) = ( g ( <. x , y >. ( comp ` ( oppCat ` D ) ) z ) f ) )
30 29 ralrimivva 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> A. f e. ( x ( Hom ` ( oppCat ` C ) ) y ) A. g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ( g ( <. x , y >. ( comp ` ( oppCat ` C ) ) z ) f ) = ( g ( <. x , y >. ( comp ` ( oppCat ` D ) ) z ) f ) )
31 30 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` ( oppCat ` C ) ) y ) A. g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ( g ( <. x , y >. ( comp ` ( oppCat ` C ) ) z ) f ) = ( g ( <. x , y >. ( comp ` ( oppCat ` D ) ) z ) f ) )
32 eqid 
 |-  ( comp ` ( oppCat ` C ) ) = ( comp ` ( oppCat ` C ) )
33 eqid 
 |-  ( comp ` ( oppCat ` D ) ) = ( comp ` ( oppCat ` D ) )
34 eqid 
 |-  ( Hom ` ( oppCat ` C ) ) = ( Hom ` ( oppCat ` C ) )
35 13 3 oppcbas 
 |-  ( Base ` C ) = ( Base ` ( oppCat ` C ) )
36 35 a1i 
 |-  ( ph -> ( Base ` C ) = ( Base ` ( oppCat ` C ) ) )
37 22 21 oppcbas 
 |-  ( Base ` D ) = ( Base ` ( oppCat ` D ) )
38 23 37 eqtrdi 
 |-  ( ph -> ( Base ` C ) = ( Base ` ( oppCat ` D ) ) )
39 1 oppchomfpropd 
 |-  ( ph -> ( Homf ` ( oppCat ` C ) ) = ( Homf ` ( oppCat ` D ) ) )
40 32 33 34 36 38 39 comfeq 
 |-  ( ph -> ( ( comf ` ( oppCat ` C ) ) = ( comf ` ( oppCat ` D ) ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` ( oppCat ` C ) ) y ) A. g e. ( y ( Hom ` ( oppCat ` C ) ) z ) ( g ( <. x , y >. ( comp ` ( oppCat ` C ) ) z ) f ) = ( g ( <. x , y >. ( comp ` ( oppCat ` D ) ) z ) f ) ) )
41 31 40 mpbird 
 |-  ( ph -> ( comf ` ( oppCat ` C ) ) = ( comf ` ( oppCat ` D ) ) )