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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
natoppf.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
natoppf.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
natoppf.m ⊢ 𝑀 = ( 𝑂 Nat 𝑃 )
natoppfb.k ⊢ ( 𝜑 → 𝐾 = ( oppFunc ‘ 𝐹 ) )
natoppfb.l ⊢ ( 𝜑 → 𝐿 = ( oppFunc ‘ 𝐺 ) )
natoppfb.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
natoppfb.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
Assertion natoppfb ( 𝜑 → ( 𝐹 𝑁 𝐺 ) = ( 𝐿 𝑀 𝐾 ) )

Proof

Step Hyp Ref Expression
1 natoppf.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 natoppf.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 natoppf.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
4 natoppf.m ⊢ 𝑀 = ( 𝑂 Nat 𝑃 )
5 natoppfb.k ⊢ ( 𝜑 → 𝐾 = ( oppFunc ‘ 𝐹 ) )
6 natoppfb.l ⊢ ( 𝜑 → 𝐿 = ( oppFunc ‘ 𝐺 ) )
7 natoppfb.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
8 natoppfb.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
9 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ) → 𝐾 = ( oppFunc ‘ 𝐹 ) )
10 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ) → 𝐿 = ( oppFunc ‘ 𝐺 ) )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ) → 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) )
12 1 2 3 4 9 10 11 natoppf2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ) → 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) )
13 eqid ⊢ ( oppCat ‘ 𝑂 ) = ( oppCat ‘ 𝑂 )
14 eqid ⊢ ( oppCat ‘ 𝑃 ) = ( oppCat ‘ 𝑃 )
15 eqid ⊢ ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) = ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐿 = ( oppFunc ‘ 𝐺 ) )
17 16 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ 𝐿 ) = ( oppFunc ‘ ( oppFunc ‘ 𝐺 ) ) )
18 4 natrcl ⊢ ( 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) → ( 𝐿 ∈ ( 𝑂 Func 𝑃 ) ∧ 𝐾 ∈ ( 𝑂 Func 𝑃 ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( 𝐿 ∈ ( 𝑂 Func 𝑃 ) ∧ 𝐾 ∈ ( 𝑂 Func 𝑃 ) ) )
20 19 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐿 ∈ ( 𝑂 Func 𝑃 ) )
21 16 20 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ 𝐺 ) ∈ ( 𝑂 Func 𝑃 ) )
22 relfunc ⊢ Rel ( 𝑂 Func 𝑃 )
23 eqid ⊢ ( oppFunc ‘ 𝐺 ) = ( oppFunc ‘ 𝐺 )
24 21 22 23 2oppf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ ( oppFunc ‘ 𝐺 ) ) = 𝐺 )
25 17 24 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐺 = ( oppFunc ‘ 𝐿 ) )
26 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐾 = ( oppFunc ‘ 𝐹 ) )
27 26 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ 𝐾 ) = ( oppFunc ‘ ( oppFunc ‘ 𝐹 ) ) )
28 19 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐾 ∈ ( 𝑂 Func 𝑃 ) )
29 26 28 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ 𝐹 ) ∈ ( 𝑂 Func 𝑃 ) )
30 eqid ⊢ ( oppFunc ‘ 𝐹 ) = ( oppFunc ‘ 𝐹 )
31 29 22 30 2oppf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppFunc ‘ ( oppFunc ‘ 𝐹 ) ) = 𝐹 )
32 27 31 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐹 = ( oppFunc ‘ 𝐾 ) )
33 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) )
34 13 14 4 15 25 32 33 natoppf2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝑥 ∈ ( 𝐹 ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) 𝐺 ) )
35 1 2oppchomf ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) )
36 35 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ 𝑂 ) ) )
37 1 2oppccomf ⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) )
38 37 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ 𝑂 ) ) )
39 2 2oppchomf ⊢ ( Homf ‘ 𝐷 ) = ( Homf ‘ ( oppCat ‘ 𝑃 ) )
40 39 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( Homf ‘ 𝐷 ) = ( Homf ‘ ( oppCat ‘ 𝑃 ) ) )
41 2 2oppccomf ⊢ ( compf ‘ 𝐷 ) = ( compf ‘ ( oppCat ‘ 𝑃 ) )
42 41 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( compf ‘ 𝐷 ) = ( compf ‘ ( oppCat ‘ 𝑃 ) ) )
43 7 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐶 ∈ 𝑉 )
44 8 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐷 ∈ 𝑊 )
45 1 2 43 44 29 funcoppc5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
46 45 func1st2nd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( 1st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2nd ‘ 𝐹 ) )
47 46 funcrcl2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐶 ∈ Cat )
48 1 oppccat ⊢ ( 𝐶 ∈ Cat → 𝑂 ∈ Cat )
49 13 oppccat ⊢ ( 𝑂 ∈ Cat → ( oppCat ‘ 𝑂 ) ∈ Cat )
50 47 48 49 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppCat ‘ 𝑂 ) ∈ Cat )
51 46 funcrcl3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝐷 ∈ Cat )
52 2 oppccat ⊢ ( 𝐷 ∈ Cat → 𝑃 ∈ Cat )
53 14 oppccat ⊢ ( 𝑃 ∈ Cat → ( oppCat ‘ 𝑃 ) ∈ Cat )
54 51 52 53 3syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( oppCat ‘ 𝑃 ) ∈ Cat )
55 36 38 40 42 47 50 51 54 natpropd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( 𝐶 Nat 𝐷 ) = ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) )
56 3 55 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝑁 = ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) )
57 56 oveqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → ( 𝐹 𝑁 𝐺 ) = ( 𝐹 ( ( oppCat ‘ 𝑂 ) Nat ( oppCat ‘ 𝑃 ) ) 𝐺 ) )
58 34 57 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) → 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) )
59 12 58 impbida ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐹 𝑁 𝐺 ) ↔ 𝑥 ∈ ( 𝐿 𝑀 𝐾 ) ) )
60 59 eqrdv ⊢ ( 𝜑 → ( 𝐹 𝑁 𝐺 ) = ( 𝐿 𝑀 𝐾 ) )