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

Metamath Proof Explorer

Theorem natoppf2

Description: A natural transformation is natural between opposite functors. (Contributed by Zhi Wang, 18-Nov-2025)

Ref Expression
Hypotheses natoppf.o 
|- O = ( oppCat ` C )
natoppf.p 
|- P = ( oppCat ` D )
natoppf.n 
|- N = ( C Nat D )
natoppf.m 
|- M = ( O Nat P )
natoppfb.k 
|- ( ph -> K = ( oppFunc ` F ) )
natoppfb.l 
|- ( ph -> L = ( oppFunc ` G ) )
natoppf2.a 
|- ( ph -> A e. ( F N G ) )
Assertion natoppf2 
|- ( ph -> A e. ( L M K ) )

Proof

Step Hyp Ref Expression
1 natoppf.o 
 |-  O = ( oppCat ` C )
2 natoppf.p 
 |-  P = ( oppCat ` D )
3 natoppf.n 
 |-  N = ( C Nat D )
4 natoppf.m 
 |-  M = ( O Nat P )
5 natoppfb.k 
 |-  ( ph -> K = ( oppFunc ` F ) )
6 natoppfb.l 
 |-  ( ph -> L = ( oppFunc ` G ) )
7 natoppf2.a 
 |-  ( ph -> A e. ( F N G ) )
8 3 7 nat1st2nd 
 |-  ( ph -> A e. ( <. ( 1st ` F ) , ( 2nd ` F ) >. N <. ( 1st ` G ) , ( 2nd ` G ) >. ) )
9 1 2 3 4 8 natoppf 
 |-  ( ph -> A e. ( <. ( 1st ` G ) , tpos ( 2nd ` G ) >. M <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) )
10 3 natrcl 
 |-  ( A e. ( F N G ) -> ( F e. ( C Func D ) /\ G e. ( C Func D ) ) )
11 10 simprd 
 |-  ( A e. ( F N G ) -> G e. ( C Func D ) )
12 oppfval2 
 |-  ( G e. ( C Func D ) -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. )
13 7 11 12 3syl 
 |-  ( ph -> ( oppFunc ` G ) = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. )
14 6 13 eqtrd 
 |-  ( ph -> L = <. ( 1st ` G ) , tpos ( 2nd ` G ) >. )
15 10 simpld 
 |-  ( A e. ( F N G ) -> F e. ( C Func D ) )
16 oppfval2 
 |-  ( F e. ( C Func D ) -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
17 7 15 16 3syl 
 |-  ( ph -> ( oppFunc ` F ) = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
18 5 17 eqtrd 
 |-  ( ph -> K = <. ( 1st ` F ) , tpos ( 2nd ` F ) >. )
19 14 18 oveq12d 
 |-  ( ph -> ( L M K ) = ( <. ( 1st ` G ) , tpos ( 2nd ` G ) >. M <. ( 1st ` F ) , tpos ( 2nd ` F ) >. ) )
20 9 19 eleqtrrd 
 |-  ( ph -> A e. ( L M K ) )