Metamath Proof Explorer

Theorem 2oppccomf

Description: The double opposite category has the same composition as the original category. Intended for use with property lemmas such as monpropd . (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypothesis oppcbas.1 
|- O = ( oppCat ` C )
Assertion 2oppccomf 
|- ( comf ` C ) = ( comf ` ( oppCat ` O ) )

Proof

Step Hyp Ref Expression
1 oppcbas.1 
 |-  O = ( oppCat ` C )
2 eqid 
 |-  ( Base ` C ) = ( Base ` C )
3 1 2 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
4 eqid 
 |-  ( comp ` O ) = ( comp ` O )
5 eqid 
 |-  ( oppCat ` O ) = ( oppCat ` O )
6 simpr1 
 |-  ( ( T. /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
7 simpr2 
 |-  ( ( T. /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
8 simpr3 
 |-  ( ( T. /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> z e. ( Base ` C ) )
9 3 4 5 6 7 8 oppcco 
 |-  ( ( T. /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> ( g ( <. x , y >. ( comp ` ( oppCat ` O ) ) z ) f ) = ( f ( <. z , y >. ( comp ` O ) x ) g ) )
10 eqid 
 |-  ( comp ` C ) = ( comp ` C )
11 2 10 1 8 7 6 oppcco 
 |-  ( ( T. /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> ( f ( <. z , y >. ( comp ` O ) x ) g ) = ( g ( <. x , y >. ( comp ` C ) z ) f ) )
12 9 11 eqtr2d 
 |-  ( ( T. /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` ( oppCat ` O ) ) z ) f ) )
13 12 ralrimivw 
 |-  ( ( T. /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) ) -> A. g e. ( y ( Hom ` C ) z ) ( g ( <. x , y >. ( comp ` C ) z ) f ) = ( g ( <. x , y >. ( comp ` ( oppCat ` O ) ) z ) f ) )
14 13 ralrimivw 
 |-  ( ( T. /\ ( 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 ` ( oppCat ` O ) ) z ) f ) )
15 14 ralrimivvva 
 |-  ( T. -> 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 ` ( oppCat ` O ) ) z ) f ) )
16 eqid 
 |-  ( comp ` ( oppCat ` O ) ) = ( comp ` ( oppCat ` O ) )
17 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
18 eqidd 
 |-  ( T. -> ( Base ` C ) = ( Base ` C ) )
19 1 2 2oppcbas 
 |-  ( Base ` C ) = ( Base ` ( oppCat ` O ) )
20 19 a1i 
 |-  ( T. -> ( Base ` C ) = ( Base ` ( oppCat ` O ) ) )
21 1 2oppchomf 
 |-  ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
22 21 a1i 
 |-  ( T. -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
23 10 16 17 18 20 22 comfeq 
 |-  ( T. -> ( ( comf ` C ) = ( comf ` ( oppCat ` 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 ` ( oppCat ` O ) ) z ) f ) ) )
24 15 23 mpbird 
 |-  ( T. -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
25 24 mptru 
 |-  ( comf ` C ) = ( comf ` ( oppCat ` O ) )