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

Metamath Proof Explorer

Theorem funcoppc3

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 )
funcoppc3.f 
|- ( ph -> F ( O Func P ) tpos G )
funcoppc3.g 
|- ( ph -> G Fn ( A X. B ) )
Assertion funcoppc3 
|- ( 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 funcoppc3.f 
 |-  ( ph -> F ( O Func P ) tpos G )
6 funcoppc3.g 
 |-  ( ph -> G Fn ( A X. B ) )
7 1 2 3 4 5 funcoppc2 
 |-  ( ph -> F ( C Func D ) tpos tpos G )
8 fnrel 
 |-  ( G Fn ( A X. B ) -> Rel G )
9 6 8 syl 
 |-  ( ph -> Rel G )
10 relxp 
 |-  Rel ( A X. B )
11 6 fndmd 
 |-  ( ph -> dom G = ( A X. B ) )
12 11 releqd 
 |-  ( ph -> ( Rel dom G <-> Rel ( A X. B ) ) )
13 10 12 mpbiri 
 |-  ( ph -> Rel dom G )
14 tpostpos2 
 |-  ( ( Rel G /\ Rel dom G ) -> tpos tpos G = G )
15 9 13 14 syl2anc 
 |-  ( ph -> tpos tpos G = G )
16 7 15 breqtrd 
 |-  ( ph -> F ( C Func D ) G )