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 ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
natoppf.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
natoppf.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
natoppf.m ⊢ 𝑀 = ( 𝑂 Nat 𝑃 )
natoppf.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
Assertion natoppf ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐾 , tpos 𝐿 ⟩ 𝑀 ⟨ 𝐹 , tpos 𝐺 ⟩ ) )

Proof

Step Hyp Ref Expression
1 natoppf.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 natoppf.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 natoppf.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
4 natoppf.m ⊢ 𝑀 = ( 𝑂 Nat 𝑃 )
5 natoppf.a ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
6 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
7 1 6 oppcbas ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
8 eqid ⊢ ( Hom ‘ 𝑂 ) = ( Hom ‘ 𝑂 )
9 eqid ⊢ ( Hom ‘ 𝑃 ) = ( Hom ‘ 𝑃 )
10 eqid ⊢ ( comp ‘ 𝑃 ) = ( comp ‘ 𝑃 )
11 3 5 natrcl3 ⊢ ( 𝜑 → 𝐾 ( 𝐶 Func 𝐷 ) 𝐿 )
12 1 2 11 funcoppc ⊢ ( 𝜑 → 𝐾 ( 𝑂 Func 𝑃 ) tpos 𝐿 )
13 3 5 natrcl2 ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
14 1 2 13 funcoppc ⊢ ( 𝜑 → 𝐹 ( 𝑂 Func 𝑃 ) tpos 𝐺 )
15 3 5 6 natfn ⊢ ( 𝜑 → 𝐴 Fn ( Base ‘ 𝐶 ) )
16 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
17 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
19 3 16 6 17 18 natcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) ) )
20 17 2 oppchom ⊢ ( ( 𝐾 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( Hom ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) )
21 19 20 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝐴 ‘ 𝑥 ) ∈ ( ( 𝐾 ‘ 𝑥 ) ( Hom ‘ 𝑃 ) ( 𝐹 ‘ 𝑥 ) ) )
22 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → 𝐴 ∈ ( ⟨ 𝐹 , 𝐺 ⟩ 𝑁 ⟨ 𝐾 , 𝐿 ⟩ ) )
23 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
24 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
25 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → 𝑦 ∈ ( Base ‘ 𝐶 ) )
26 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
27 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) )
28 23 1 oppchom ⊢ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 )
29 27 28 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → 𝑚 ∈ ( 𝑦 ( Hom ‘ 𝐶 ) 𝑥 ) )
30 3 22 6 23 24 25 26 29 nati ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → ( ( 𝐴 ‘ 𝑥 ) ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) ) ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑚 ) ) = ( ( ( 𝑦 𝐿 𝑥 ) ‘ 𝑚 ) ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) ) ( 𝐴 ‘ 𝑦 ) ) )
31 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
32 6 31 11 funcf1 ⊢ ( 𝜑 → 𝐾 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
33 32 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → 𝐾 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
34 33 26 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → ( 𝐾 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
35 6 31 13 funcf1 ⊢ ( 𝜑 → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
36 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → 𝐹 : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
37 36 26 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
38 36 25 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
39 31 24 2 34 37 38 oppcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → ( ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑚 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) = ( ( 𝐴 ‘ 𝑥 ) ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐹 ‘ 𝑥 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) ) ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑚 ) ) )
40 33 25 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → ( 𝐾 ‘ 𝑦 ) ∈ ( Base ‘ 𝐷 ) )
41 31 24 2 34 40 38 oppcco ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( ( 𝑦 𝐿 𝑥 ) ‘ 𝑚 ) ) = ( ( ( 𝑦 𝐿 𝑥 ) ‘ 𝑚 ) ( ⟨ ( 𝐹 ‘ 𝑦 ) , ( 𝐾 ‘ 𝑦 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐾 ‘ 𝑥 ) ) ( 𝐴 ‘ 𝑦 ) ) )
42 30 39 41 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( ( 𝑦 𝐿 𝑥 ) ‘ 𝑚 ) ) = ( ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑚 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) )
43 ovtpos ⊢ ( 𝑥 tpos 𝐿 𝑦 ) = ( 𝑦 𝐿 𝑥 )
44 43 fveq1i ⊢ ( ( 𝑥 tpos 𝐿 𝑦 ) ‘ 𝑚 ) = ( ( 𝑦 𝐿 𝑥 ) ‘ 𝑚 )
45 44 oveq2i ⊢ ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( ( 𝑥 tpos 𝐿 𝑦 ) ‘ 𝑚 ) ) = ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( ( 𝑦 𝐿 𝑥 ) ‘ 𝑚 ) )
46 ovtpos ⊢ ( 𝑥 tpos 𝐺 𝑦 ) = ( 𝑦 𝐺 𝑥 )
47 46 fveq1i ⊢ ( ( 𝑥 tpos 𝐺 𝑦 ) ‘ 𝑚 ) = ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑚 )
48 47 oveq1i ⊢ ( ( ( 𝑥 tpos 𝐺 𝑦 ) ‘ 𝑚 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) = ( ( ( 𝑦 𝐺 𝑥 ) ‘ 𝑚 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) )
49 42 45 48 3eqtr4g ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ 𝑦 ∈ ( Base ‘ 𝐶 ) ) ) ∧ 𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑂 ) 𝑦 ) ) → ( ( 𝐴 ‘ 𝑦 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐾 ‘ 𝑦 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( ( 𝑥 tpos 𝐿 𝑦 ) ‘ 𝑚 ) ) = ( ( ( 𝑥 tpos 𝐺 𝑦 ) ‘ 𝑚 ) ( ⟨ ( 𝐾 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) ⟩ ( comp ‘ 𝑃 ) ( 𝐹 ‘ 𝑦 ) ) ( 𝐴 ‘ 𝑥 ) ) )
50 4 7 8 9 10 12 14 15 21 49 isnatd ⊢ ( 𝜑 → 𝐴 ∈ ( ⟨ 𝐾 , tpos 𝐿 ⟩ 𝑀 ⟨ 𝐹 , tpos 𝐺 ⟩ ) )