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

Metamath Proof Explorer

Theorem funcoppc4

Description: A functor on opposite categories yields a functor on the original categories. (Contributed by Zhi Wang, 14-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 )
funcoppc4.f 
|- ( ph -> ( F oppFunc G ) e. ( O Func P ) )
Assertion funcoppc4 
|- ( ph -> F ( C Func D ) 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 funcoppc4.f 
 |-  ( ph -> ( F oppFunc G ) e. ( O Func P ) )
6 5 func1st2nd 
 |-  ( ph -> ( 1st ` ( F oppFunc G ) ) ( O Func P ) ( 2nd ` ( F oppFunc G ) ) )
7 1 2 3 4 6 funcoppc2 
 |-  ( ph -> ( 1st ` ( F oppFunc G ) ) ( C Func D ) tpos ( 2nd ` ( F oppFunc G ) ) )
8 relfunc 
 |-  Rel ( O Func P )
9 df-ov 
 |-  ( F oppFunc G ) = ( oppFunc ` <. F , G >. )
10 eqidd 
 |-  ( ph -> <. F , G >. = <. F , G >. )
11 5 8 9 10 oppf1st2nd 
 |-  ( ph -> ( ( F oppFunc G ) e. ( _V X. _V ) /\ ( ( 1st ` ( F oppFunc G ) ) = F /\ ( 2nd ` ( F oppFunc G ) ) = tpos G ) ) )
12 11 simprld 
 |-  ( ph -> ( 1st ` ( F oppFunc G ) ) = F )
13 11 simprrd 
 |-  ( ph -> ( 2nd ` ( F oppFunc G ) ) = tpos G )
14 13 tposeqd 
 |-  ( ph -> tpos ( 2nd ` ( F oppFunc G ) ) = tpos tpos G )
15 5 8 9 10 oppfrcl3 
 |-  ( ph -> ( Rel G /\ Rel dom G ) )
16 tpostpos2 
 |-  ( ( Rel G /\ Rel dom G ) -> tpos tpos G = G )
17 15 16 syl 
 |-  ( ph -> tpos tpos G = G )
18 14 17 eqtrd 
 |-  ( ph -> tpos ( 2nd ` ( F oppFunc G ) ) = G )
19 7 12 18 3brtr3d 
 |-  ( ph -> F ( C Func D ) G )