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

Metamath Proof Explorer

Theorem oppfoppc2

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

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

Proof

Step Hyp Ref Expression
1 oppfoppc.o 
 |-  O = ( oppCat ` C )
2 oppfoppc.p 
 |-  P = ( oppCat ` D )
3 oppfoppc2.f 
 |-  ( ph -> F e. ( C Func D ) )
4 relfunc 
 |-  Rel ( C Func D )
5 1st2nd 
 |-  ( ( Rel ( C Func D ) /\ F e. ( C Func D ) ) -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
6 4 3 5 sylancr 
 |-  ( ph -> F = <. ( 1st ` F ) , ( 2nd ` F ) >. )
7 6 fveq2d 
 |-  ( ph -> ( oppFunc ` F ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. ) )
8 df-ov 
 |-  ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) = ( oppFunc ` <. ( 1st ` F ) , ( 2nd ` F ) >. )
9 7 8 eqtr4di 
 |-  ( ph -> ( oppFunc ` F ) = ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) )
10 3 func1st2nd 
 |-  ( ph -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
11 1 2 10 oppfoppc 
 |-  ( ph -> ( ( 1st ` F ) oppFunc ( 2nd ` F ) ) e. ( O Func P ) )
12 9 11 eqeltrd 
 |-  ( ph -> ( oppFunc ` F ) e. ( O Func P ) )