Metamath Proof Explorer

Theorem funcoppc

Description: A functor on categories yields a functor on the opposite categories (in the same direction), see definition 3.41 of Adamek p. 39. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses funcoppc.o 
|- O = ( oppCat ` C )
funcoppc.p 
|- P = ( oppCat ` D )
funcoppc.f 
|- ( ph -> F ( C Func D ) G )
Assertion funcoppc 
|- ( ph -> F ( O Func P ) tpos G )

Proof

Step Hyp Ref Expression
1 funcoppc.o 
 |-  O = ( oppCat ` C )
2 funcoppc.p 
 |-  P = ( oppCat ` D )
3 funcoppc.f 
 |-  ( ph -> F ( C Func D ) G )
4 eqid 
 |-  ( Base ` C ) = ( Base ` C )
5 1 4 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
6 eqid 
 |-  ( Base ` D ) = ( Base ` D )
7 2 6 oppcbas 
 |-  ( Base ` D ) = ( Base ` P )
8 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
9 eqid 
 |-  ( Hom ` P ) = ( Hom ` P )
10 eqid 
 |-  ( Id ` O ) = ( Id ` O )
11 eqid 
 |-  ( Id ` P ) = ( Id ` P )
12 eqid 
 |-  ( comp ` O ) = ( comp ` O )
13 eqid 
 |-  ( comp ` P ) = ( comp ` P )
14 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
15 3 14 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
16 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
17 15 16 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
18 17 simpld 
 |-  ( ph -> C e. Cat )
19 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
20 18 19 syl 
 |-  ( ph -> O e. Cat )
21 2 oppccat 
 |-  ( D e. Cat -> P e. Cat )
22 17 21 simpl2im 
 |-  ( ph -> P e. Cat )
23 4 6 3 funcf1 
 |-  ( ph -> F : ( Base ` C ) --> ( Base ` D ) )
24 4 3 funcfn2 
 |-  ( ph -> G Fn ( ( Base ` C ) X. ( Base ` C ) ) )
25 tposfn 
 |-  ( G Fn ( ( Base ` C ) X. ( Base ` C ) ) -> tpos G Fn ( ( Base ` C ) X. ( Base ` C ) ) )
26 24 25 syl 
 |-  ( ph -> tpos G Fn ( ( Base ` C ) X. ( Base ` C ) ) )
27 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
28 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
29 3 adantr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> F ( C Func D ) G )
30 simprr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> y e. ( Base ` C ) )
31 simprl 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> x e. ( Base ` C ) )
32 4 27 28 29 30 31 funcf2 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( y G x ) : ( y ( Hom ` C ) x ) --> ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) )
33 ovtpos 
 |-  ( x tpos G y ) = ( y G x )
34 33 feq1i 
 |-  ( ( x tpos G y ) : ( x ( Hom ` O ) y ) --> ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) <-> ( y G x ) : ( x ( Hom ` O ) y ) --> ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) )
35 27 1 oppchom 
 |-  ( x ( Hom ` O ) y ) = ( y ( Hom ` C ) x )
36 28 2 oppchom 
 |-  ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) = ( ( F ` y ) ( Hom ` D ) ( F ` x ) )
37 35 36 feq23i 
 |-  ( ( y G x ) : ( x ( Hom ` O ) y ) --> ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) <-> ( y G x ) : ( y ( Hom ` C ) x ) --> ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) )
38 34 37 bitri 
 |-  ( ( x tpos G y ) : ( x ( Hom ` O ) y ) --> ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) <-> ( y G x ) : ( y ( Hom ` C ) x ) --> ( ( F ` y ) ( Hom ` D ) ( F ` x ) ) )
39 32 38 sylibr 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) -> ( x tpos G y ) : ( x ( Hom ` O ) y ) --> ( ( F ` x ) ( Hom ` P ) ( F ` y ) ) )
40 eqid 
 |-  ( Id ` C ) = ( Id ` C )
41 eqid 
 |-  ( Id ` D ) = ( Id ` D )
42 3 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> F ( C Func D ) G )
43 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
44 4 40 41 42 43 funcid 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x G x ) ` ( ( Id ` C ) ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) )
45 ovtpos 
 |-  ( x tpos G x ) = ( x G x )
46 45 a1i 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( x tpos G x ) = ( x G x ) )
47 1 40 oppcid 
 |-  ( C e. Cat -> ( Id ` O ) = ( Id ` C ) )
48 18 47 syl 
 |-  ( ph -> ( Id ` O ) = ( Id ` C ) )
49 48 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( Id ` O ) = ( Id ` C ) )
50 49 fveq1d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` O ) ` x ) = ( ( Id ` C ) ` x ) )
51 46 50 fveq12d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x tpos G x ) ` ( ( Id ` O ) ` x ) ) = ( ( x G x ) ` ( ( Id ` C ) ` x ) ) )
52 2 41 oppcid 
 |-  ( D e. Cat -> ( Id ` P ) = ( Id ` D ) )
53 17 52 simpl2im 
 |-  ( ph -> ( Id ` P ) = ( Id ` D ) )
54 53 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( Id ` P ) = ( Id ` D ) )
55 54 fveq1d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( Id ` P ) ` ( F ` x ) ) = ( ( Id ` D ) ` ( F ` x ) ) )
56 44 51 55 3eqtr4d 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( ( x tpos G x ) ` ( ( Id ` O ) ` x ) ) = ( ( Id ` P ) ` ( F ` x ) ) )
57 eqid 
 |-  ( comp ` C ) = ( comp ` C )
58 eqid 
 |-  ( comp ` D ) = ( comp ` D )
59 3 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> F ( C Func D ) G )
60 simp23 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> z e. ( Base ` C ) )
61 simp22 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> y e. ( Base ` C ) )
62 simp21 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> x e. ( Base ` C ) )
63 simp3r 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> g e. ( y ( Hom ` O ) z ) )
64 27 1 oppchom 
 |-  ( y ( Hom ` O ) z ) = ( z ( Hom ` C ) y )
65 63 64 eleqtrdi 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> g e. ( z ( Hom ` C ) y ) )
66 simp3l 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> f e. ( x ( Hom ` O ) y ) )
67 66 35 eleqtrdi 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> f e. ( y ( Hom ` C ) x ) )
68 4 27 57 58 59 60 61 62 65 67 funcco 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> ( ( z G x ) ` ( f ( <. z , y >. ( comp ` C ) x ) g ) ) = ( ( ( y G x ) ` f ) ( <. ( F ` z ) , ( F ` y ) >. ( comp ` D ) ( F ` x ) ) ( ( z G y ) ` g ) ) )
69 4 57 1 62 61 60 oppcco 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> ( g ( <. x , y >. ( comp ` O ) z ) f ) = ( f ( <. z , y >. ( comp ` C ) x ) g ) )
70 69 fveq2d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> ( ( z G x ) ` ( g ( <. x , y >. ( comp ` O ) z ) f ) ) = ( ( z G x ) ` ( f ( <. z , y >. ( comp ` C ) x ) g ) ) )
71 23 3ad2ant1 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> F : ( Base ` C ) --> ( Base ` D ) )
72 71 62 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> ( F ` x ) e. ( Base ` D ) )
73 71 61 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> ( F ` y ) e. ( Base ` D ) )
74 71 60 ffvelrnd 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> ( F ` z ) e. ( Base ` D ) )
75 6 58 2 72 73 74 oppcco 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> ( ( ( z G y ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` P ) ( F ` z ) ) ( ( y G x ) ` f ) ) = ( ( ( y G x ) ` f ) ( <. ( F ` z ) , ( F ` y ) >. ( comp ` D ) ( F ` x ) ) ( ( z G y ) ` g ) ) )
76 68 70 75 3eqtr4d 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> ( ( z G x ) ` ( g ( <. x , y >. ( comp ` O ) z ) f ) ) = ( ( ( z G y ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` P ) ( F ` z ) ) ( ( y G x ) ` f ) ) )
77 ovtpos 
 |-  ( x tpos G z ) = ( z G x )
78 77 fveq1i 
 |-  ( ( x tpos G z ) ` ( g ( <. x , y >. ( comp ` O ) z ) f ) ) = ( ( z G x ) ` ( g ( <. x , y >. ( comp ` O ) z ) f ) )
79 ovtpos 
 |-  ( y tpos G z ) = ( z G y )
80 79 fveq1i 
 |-  ( ( y tpos G z ) ` g ) = ( ( z G y ) ` g )
81 33 fveq1i 
 |-  ( ( x tpos G y ) ` f ) = ( ( y G x ) ` f )
82 80 81 oveq12i 
 |-  ( ( ( y tpos G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` P ) ( F ` z ) ) ( ( x tpos G y ) ` f ) ) = ( ( ( z G y ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` P ) ( F ` z ) ) ( ( y G x ) ` f ) )
83 76 78 82 3eqtr4g 
 |-  ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) /\ z e. ( Base ` C ) ) /\ ( f e. ( x ( Hom ` O ) y ) /\ g e. ( y ( Hom ` O ) z ) ) ) -> ( ( x tpos G z ) ` ( g ( <. x , y >. ( comp ` O ) z ) f ) ) = ( ( ( y tpos G z ) ` g ) ( <. ( F ` x ) , ( F ` y ) >. ( comp ` P ) ( F ` z ) ) ( ( x tpos G y ) ` f ) ) )
84 5 7 8 9 10 11 12 13 20 22 23 26 39 56 83 isfuncd 
 |-  ( ph -> F ( O Func P ) tpos G )