This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oppfoppc

Description: The opposite functor is a functor on opposite categories. (Contributed by Zhi Wang, 4-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 oppfoppc.o 
 |-  O = ( oppCat ` C )
2 oppfoppc.p 
 |-  P = ( oppCat ` D )
3 oppfoppc.f 
 |-  ( ph -> F ( C Func D ) G )
4 oppfval 
 |-  ( F ( C Func D ) G -> ( F oppFunc G ) = <. F , tpos G >. )
5 3 4 syl 
 |-  ( ph -> ( F oppFunc G ) = <. F , tpos G >. )
6 1 2 3 funcoppc 
 |-  ( ph -> F ( O Func P ) tpos G )
7 df-br 
 |-  ( F ( O Func P ) tpos G <-> <. F , tpos G >. e. ( O Func P ) )
8 6 7 sylib 
 |-  ( ph -> <. F , tpos G >. e. ( O Func P ) )
9 5 8 eqeltrd 
 |-  ( ph -> ( F oppFunc G ) e. ( O Func P ) )