Metamath Proof Explorer

Theorem natoppf

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 )
natoppf.a 
|- ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
Assertion natoppf 
|- ( ph -> A e. ( <. K , tpos L >. M <. F , tpos G >. ) )

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 natoppf.a 
 |-  ( ph -> A e. ( <. F , G >. N <. K , L >. ) )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 1 6 oppcbas 
 |-  ( Base ` C ) = ( Base ` O )
8 eqid 
 |-  ( Hom ` O ) = ( Hom ` O )
9 eqid 
 |-  ( Hom ` P ) = ( Hom ` P )
10 eqid 
 |-  ( comp ` P ) = ( comp ` P )
11 3 5 natrcl3 
 |-  ( ph -> K ( C Func D ) L )
12 1 2 11 funcoppc 
 |-  ( ph -> K ( O Func P ) tpos L )
13 3 5 natrcl2 
 |-  ( ph -> F ( C Func D ) G )
14 1 2 13 funcoppc 
 |-  ( ph -> F ( O Func P ) tpos G )
15 3 5 6 natfn 
 |-  ( ph -> A Fn ( Base ` C ) )
16 5 adantr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> A e. ( <. F , G >. N <. K , L >. ) )
17 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
18 simpr 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> x e. ( Base ` C ) )
19 3 16 6 17 18 natcl 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( A ` x ) e. ( ( F ` x ) ( Hom ` D ) ( K ` x ) ) )
20 17 2 oppchom 
 |-  ( ( K ` x ) ( Hom ` P ) ( F ` x ) ) = ( ( F ` x ) ( Hom ` D ) ( K ` x ) )
21 19 20 eleqtrrdi 
 |-  ( ( ph /\ x e. ( Base ` C ) ) -> ( A ` x ) e. ( ( K ` x ) ( Hom ` P ) ( F ` x ) ) )
22 5 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> A e. ( <. F , G >. N <. K , L >. ) )
23 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
24 eqid 
 |-  ( comp ` D ) = ( comp ` D )
25 simplrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> y e. ( Base ` C ) )
26 simplrl 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> x e. ( Base ` C ) )
27 simpr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> m e. ( x ( Hom ` O ) y ) )
28 23 1 oppchom 
 |-  ( x ( Hom ` O ) y ) = ( y ( Hom ` C ) x )
29 27 28 eleqtrdi 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> m e. ( y ( Hom ` C ) x ) )
30 3 22 6 23 24 25 26 29 nati 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> ( ( A ` x ) ( <. ( F ` y ) , ( F ` x ) >. ( comp ` D ) ( K ` x ) ) ( ( y G x ) ` m ) ) = ( ( ( y L x ) ` m ) ( <. ( F ` y ) , ( K ` y ) >. ( comp ` D ) ( K ` x ) ) ( A ` y ) ) )
31 eqid 
 |-  ( Base ` D ) = ( Base ` D )
32 6 31 11 funcf1 
 |-  ( ph -> K : ( Base ` C ) --> ( Base ` D ) )
33 32 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> K : ( Base ` C ) --> ( Base ` D ) )
34 33 26 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> ( K ` x ) e. ( Base ` D ) )
35 6 31 13 funcf1 
 |-  ( ph -> F : ( Base ` C ) --> ( Base ` D ) )
36 35 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> F : ( Base ` C ) --> ( Base ` D ) )
37 36 26 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> ( F ` x ) e. ( Base ` D ) )
38 36 25 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> ( F ` y ) e. ( Base ` D ) )
39 31 24 2 34 37 38 oppcco 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> ( ( ( y G x ) ` m ) ( <. ( K ` x ) , ( F ` x ) >. ( comp ` P ) ( F ` y ) ) ( A ` x ) ) = ( ( A ` x ) ( <. ( F ` y ) , ( F ` x ) >. ( comp ` D ) ( K ` x ) ) ( ( y G x ) ` m ) ) )
40 33 25 ffvelcdmd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> ( K ` y ) e. ( Base ` D ) )
41 31 24 2 34 40 38 oppcco 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> ( ( A ` y ) ( <. ( K ` x ) , ( K ` y ) >. ( comp ` P ) ( F ` y ) ) ( ( y L x ) ` m ) ) = ( ( ( y L x ) ` m ) ( <. ( F ` y ) , ( K ` y ) >. ( comp ` D ) ( K ` x ) ) ( A ` y ) ) )
42 30 39 41 3eqtr4rd 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> ( ( A ` y ) ( <. ( K ` x ) , ( K ` y ) >. ( comp ` P ) ( F ` y ) ) ( ( y L x ) ` m ) ) = ( ( ( y G x ) ` m ) ( <. ( K ` x ) , ( F ` x ) >. ( comp ` P ) ( F ` y ) ) ( A ` x ) ) )
43 ovtpos 
 |-  ( x tpos L y ) = ( y L x )
44 43 fveq1i 
 |-  ( ( x tpos L y ) ` m ) = ( ( y L x ) ` m )
45 44 oveq2i 
 |-  ( ( A ` y ) ( <. ( K ` x ) , ( K ` y ) >. ( comp ` P ) ( F ` y ) ) ( ( x tpos L y ) ` m ) ) = ( ( A ` y ) ( <. ( K ` x ) , ( K ` y ) >. ( comp ` P ) ( F ` y ) ) ( ( y L x ) ` m ) )
46 ovtpos 
 |-  ( x tpos G y ) = ( y G x )
47 46 fveq1i 
 |-  ( ( x tpos G y ) ` m ) = ( ( y G x ) ` m )
48 47 oveq1i 
 |-  ( ( ( x tpos G y ) ` m ) ( <. ( K ` x ) , ( F ` x ) >. ( comp ` P ) ( F ` y ) ) ( A ` x ) ) = ( ( ( y G x ) ` m ) ( <. ( K ` x ) , ( F ` x ) >. ( comp ` P ) ( F ` y ) ) ( A ` x ) )
49 42 45 48 3eqtr4g 
 |-  ( ( ( ph /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) ) /\ m e. ( x ( Hom ` O ) y ) ) -> ( ( A ` y ) ( <. ( K ` x ) , ( K ` y ) >. ( comp ` P ) ( F ` y ) ) ( ( x tpos L y ) ` m ) ) = ( ( ( x tpos G y ) ` m ) ( <. ( K ` x ) , ( F ` x ) >. ( comp ` P ) ( F ` y ) ) ( A ` x ) ) )
50 4 7 8 9 10 12 14 15 21 49 isnatd 
 |-  ( ph -> A e. ( <. K , tpos L >. M <. F , tpos G >. ) )