Metamath Proof Explorer

Theorem funcoppc2

Description: A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 4-Nov-2025)

Ref Expression
Hypotheses funcoppc2.o 
|- O = ( oppCat ` C )
funcoppc2.p 
|- P = ( oppCat ` D )
funcoppc2.c 
|- ( ph -> C e. V )
funcoppc2.d 
|- ( ph -> D e. W )
funcoppc2.f 
|- ( ph -> F ( O Func P ) G )
Assertion funcoppc2 
|- ( ph -> F ( C Func D ) tpos G )

Proof

Step Hyp Ref Expression
1 funcoppc2.o 
 |-  O = ( oppCat ` C )
2 funcoppc2.p 
 |-  P = ( oppCat ` D )
3 funcoppc2.c 
 |-  ( ph -> C e. V )
4 funcoppc2.d 
 |-  ( ph -> D e. W )
5 funcoppc2.f 
 |-  ( ph -> F ( O Func P ) G )
6 eqid 
 |-  ( oppCat ` O ) = ( oppCat ` O )
7 eqid 
 |-  ( oppCat ` P ) = ( oppCat ` P )
8 6 7 5 funcoppc 
 |-  ( ph -> F ( ( oppCat ` O ) Func ( oppCat ` P ) ) tpos G )
9 1 2oppchomf 
 |-  ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
10 9 a1i 
 |-  ( ph -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
11 1 2oppccomf 
 |-  ( comf ` C ) = ( comf ` ( oppCat ` O ) )
12 11 a1i 
 |-  ( ph -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
13 2 2oppchomf 
 |-  ( Homf ` D ) = ( Homf ` ( oppCat ` P ) )
14 13 a1i 
 |-  ( ph -> ( Homf ` D ) = ( Homf ` ( oppCat ` P ) ) )
15 2 2oppccomf 
 |-  ( comf ` D ) = ( comf ` ( oppCat ` P ) )
16 15 a1i 
 |-  ( ph -> ( comf ` D ) = ( comf ` ( oppCat ` P ) ) )
17 3 elexd 
 |-  ( ph -> C e. _V )
18 fvexd 
 |-  ( ph -> ( oppCat ` O ) e. _V )
19 4 elexd 
 |-  ( ph -> D e. _V )
20 fvexd 
 |-  ( ph -> ( oppCat ` P ) e. _V )
21 10 12 14 16 17 18 19 20 funcpropd 
 |-  ( ph -> ( C Func D ) = ( ( oppCat ` O ) Func ( oppCat ` P ) ) )
22 21 breqd 
 |-  ( ph -> ( F ( C Func D ) tpos G <-> F ( ( oppCat ` O ) Func ( oppCat ` P ) ) tpos G ) )
23 8 22 mpbird 
 |-  ( ph -> F ( C Func D ) tpos G )