Metamath Proof Explorer

Theorem oppcthinco

Description: If the opposite category of a thin category has the same base and hom-sets as the original category, then it has the same composition operation as the original category. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses oppcthinco.o 
|- O = ( oppCat ` C )
oppcthinco.c 
|- ( ph -> C e. ThinCat )
oppcthinco.1 
|- ( ph -> ( Homf ` C ) = ( Homf ` O ) )
Assertion oppcthinco 
|- ( ph -> ( comf ` C ) = ( comf ` O ) )

Proof

Step Hyp Ref Expression
1 oppcthinco.o 
 |-  O = ( oppCat ` C )
2 oppcthinco.c 
 |-  ( ph -> C e. ThinCat )
3 oppcthinco.1 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` O ) )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 eqid 
 |-  ( comp ` C ) = ( comp ` C )
6 simplr1 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> x e. ( Base ` C ) )
7 simplr2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> y e. ( Base ` C ) )
8 simplr3 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> z e. ( Base ` C ) )
9 4 5 1 6 7 8 oppcco 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( g ( <. x , y >. ( comp ` O ) z ) f ) = ( f ( <. z , y >. ( comp ` C ) x ) g ) )
10 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
11 2 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> C e. ThinCat )
12 11 thinccd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> C e. Cat )
13 simprr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> g e. ( y ( Hom ` C ) z ) )
14 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
15 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( Homf ` C ) = ( Homf ` O ) )
16 4 10 14 15 7 8 homfeqval 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( y ( Hom ` C ) z ) = ( y ( Hom ` O ) z ) )
17 10 1 oppchom 
 |-  ( y ( Hom ` O ) z ) = ( z ( Hom ` C ) y )
18 16 17 eqtrdi 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( y ( Hom ` C ) z ) = ( z ( Hom ` C ) y ) )
19 13 18 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> g e. ( z ( Hom ` C ) y ) )
20 simprl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> f e. ( x ( Hom ` C ) y ) )
21 4 10 14 15 6 7 homfeqval 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x ( Hom ` C ) y ) = ( x ( Hom ` O ) y ) )
22 10 1 oppchom 
 |-  ( x ( Hom ` O ) y ) = ( y ( Hom ` C ) x )
23 21 22 eqtrdi 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x ( Hom ` C ) y ) = ( y ( Hom ` C ) x ) )
24 20 23 eleqtrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> f e. ( y ( Hom ` C ) x ) )
25 4 10 5 12 8 7 6 19 24 catcocl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( f ( <. z , y >. ( comp ` C ) x ) g ) e. ( z ( Hom ` C ) x ) )
26 4 10 14 15 6 8 homfeqval 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x ( Hom ` C ) z ) = ( x ( Hom ` O ) z ) )
27 10 1 oppchom 
 |-  ( x ( Hom ` O ) z ) = ( z ( Hom ` C ) x )
28 26 27 eqtrdi 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( x ( Hom ` C ) z ) = ( z ( Hom ` C ) x ) )
29 25 28 eleqtrrd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( f ( <. z , y >. ( comp ` C ) x ) g ) e. ( x ( Hom ` C ) z ) )
30 4 10 5 12 6 7 8 20 13 catcocl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) e. ( x ( Hom ` C ) z ) )
31 6 8 29 30 4 10 11 thincmo2 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( f ( <. z , y >. ( comp ` C ) x ) g ) = ( g ( <. x , y >. ( comp ` C ) z ) f ) )
32 9 31 eqtr2d 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) /\ ( f e. ( x ( Hom ` C ) y ) /\ g e. ( y ( Hom ` C ) z ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` O ) z ) f ) )
33 32 ralrimivva 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` O ) z ) f ) )
34 33 ralrimivvva 
 |-  ( ph -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` O ) z ) f ) )
35 eqid 
 |-  ( comp ` O ) = ( comp ` O )
36 eqidd 
 |-  ( ph -> ( Base ` C ) = ( Base ` C ) )
37 3 homfeqbas 
 |-  ( ph -> ( Base ` C ) = ( Base ` O ) )
38 5 35 10 36 37 3 comfeq 
 |-  ( ph -> ( ( comf ` C ) = ( comf ` O ) <-> A. x e. ( Base ` C ) A. y e. ( Base ` C ) A. z e. ( Base ` C ) A. f e. ( x ( Hom ` C ) y ) A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` O ) z ) f ) ) )
39 34 38 mpbird 
 |-  ( ph -> ( comf ` C ) = ( comf ` O ) )