Metamath Proof Explorer

Theorem natoppfb

Description: A natural transformation is natural between opposite functors, and vice versa. (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 ) )
natoppfb.c 
|- ( ph -> C e. V )
natoppfb.d 
|- ( ph -> D e. W )
Assertion natoppfb 
|- ( ph -> ( F N G ) = ( 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 natoppfb.c 
 |-  ( ph -> C e. V )
8 natoppfb.d 
 |-  ( ph -> D e. W )
9 5 adantr 
 |-  ( ( ph /\ x e. ( F N G ) ) -> K = ( oppFunc ` F ) )
10 6 adantr 
 |-  ( ( ph /\ x e. ( F N G ) ) -> L = ( oppFunc ` G ) )
11 simpr 
 |-  ( ( ph /\ x e. ( F N G ) ) -> x e. ( F N G ) )
12 1 2 3 4 9 10 11 natoppf2 
 |-  ( ( ph /\ x e. ( F N G ) ) -> x e. ( L M K ) )
13 eqid 
 |-  ( oppCat ` O ) = ( oppCat ` O )
14 eqid 
 |-  ( oppCat ` P ) = ( oppCat ` P )
15 eqid 
 |-  ( ( oppCat ` O ) Nat ( oppCat ` P ) ) = ( ( oppCat ` O ) Nat ( oppCat ` P ) )
16 6 adantr 
 |-  ( ( ph /\ x e. ( L M K ) ) -> L = ( oppFunc ` G ) )
17 16 fveq2d 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` L ) = ( oppFunc ` ( oppFunc ` G ) ) )
18 4 natrcl 
 |-  ( x e. ( L M K ) -> ( L e. ( O Func P ) /\ K e. ( O Func P ) ) )
19 18 adantl 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( L e. ( O Func P ) /\ K e. ( O Func P ) ) )
20 19 simpld 
 |-  ( ( ph /\ x e. ( L M K ) ) -> L e. ( O Func P ) )
21 16 20 eqeltrrd 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` G ) e. ( O Func P ) )
22 relfunc 
 |-  Rel ( O Func P )
23 eqid 
 |-  ( oppFunc ` G ) = ( oppFunc ` G )
24 21 22 23 2oppf 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` ( oppFunc ` G ) ) = G )
25 17 24 eqtr2d 
 |-  ( ( ph /\ x e. ( L M K ) ) -> G = ( oppFunc ` L ) )
26 5 adantr 
 |-  ( ( ph /\ x e. ( L M K ) ) -> K = ( oppFunc ` F ) )
27 26 fveq2d 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` K ) = ( oppFunc ` ( oppFunc ` F ) ) )
28 19 simprd 
 |-  ( ( ph /\ x e. ( L M K ) ) -> K e. ( O Func P ) )
29 26 28 eqeltrrd 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` F ) e. ( O Func P ) )
30 eqid 
 |-  ( oppFunc ` F ) = ( oppFunc ` F )
31 29 22 30 2oppf 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( oppFunc ` ( oppFunc ` F ) ) = F )
32 27 31 eqtr2d 
 |-  ( ( ph /\ x e. ( L M K ) ) -> F = ( oppFunc ` K ) )
33 simpr 
 |-  ( ( ph /\ x e. ( L M K ) ) -> x e. ( L M K ) )
34 13 14 4 15 25 32 33 natoppf2 
 |-  ( ( ph /\ x e. ( L M K ) ) -> x e. ( F ( ( oppCat ` O ) Nat ( oppCat ` P ) ) G ) )
35 1 2oppchomf 
 |-  ( Homf ` C ) = ( Homf ` ( oppCat ` O ) )
36 35 a1i 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( Homf ` C ) = ( Homf ` ( oppCat ` O ) ) )
37 1 2oppccomf 
 |-  ( comf ` C ) = ( comf ` ( oppCat ` O ) )
38 37 a1i 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( comf ` C ) = ( comf ` ( oppCat ` O ) ) )
39 2 2oppchomf 
 |-  ( Homf ` D ) = ( Homf ` ( oppCat ` P ) )
40 39 a1i 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( Homf ` D ) = ( Homf ` ( oppCat ` P ) ) )
41 2 2oppccomf 
 |-  ( comf ` D ) = ( comf ` ( oppCat ` P ) )
42 41 a1i 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( comf ` D ) = ( comf ` ( oppCat ` P ) ) )
43 7 adantr 
 |-  ( ( ph /\ x e. ( L M K ) ) -> C e. V )
44 8 adantr 
 |-  ( ( ph /\ x e. ( L M K ) ) -> D e. W )
45 1 2 43 44 29 funcoppc5 
 |-  ( ( ph /\ x e. ( L M K ) ) -> F e. ( C Func D ) )
46 45 func1st2nd 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( 1st ` F ) ( C Func D ) ( 2nd ` F ) )
47 46 funcrcl2 
 |-  ( ( ph /\ x e. ( L M K ) ) -> C e. Cat )
48 1 oppccat 
 |-  ( C e. Cat -> O e. Cat )
49 13 oppccat 
 |-  ( O e. Cat -> ( oppCat ` O ) e. Cat )
50 47 48 49 3syl 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( oppCat ` O ) e. Cat )
51 46 funcrcl3 
 |-  ( ( ph /\ x e. ( L M K ) ) -> D e. Cat )
52 2 oppccat 
 |-  ( D e. Cat -> P e. Cat )
53 14 oppccat 
 |-  ( P e. Cat -> ( oppCat ` P ) e. Cat )
54 51 52 53 3syl 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( oppCat ` P ) e. Cat )
55 36 38 40 42 47 50 51 54 natpropd 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( C Nat D ) = ( ( oppCat ` O ) Nat ( oppCat ` P ) ) )
56 3 55 eqtrid 
 |-  ( ( ph /\ x e. ( L M K ) ) -> N = ( ( oppCat ` O ) Nat ( oppCat ` P ) ) )
57 56 oveqd 
 |-  ( ( ph /\ x e. ( L M K ) ) -> ( F N G ) = ( F ( ( oppCat ` O ) Nat ( oppCat ` P ) ) G ) )
58 34 57 eleqtrrd 
 |-  ( ( ph /\ x e. ( L M K ) ) -> x e. ( F N G ) )
59 12 58 impbida 
 |-  ( ph -> ( x e. ( F N G ) <-> x e. ( L M K ) ) )
60 59 eqrdv 
 |-  ( ph -> ( F N G ) = ( L M K ) )