Metamath Proof Explorer

Theorem fucoppc

Description: The isomorphism from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 18-Nov-2025)

Ref Expression
Hypotheses fucoppc.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
fucoppc.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
fucoppc.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
fucoppc.r ⊢ 𝑅 = ( oppCat ‘ 𝑄 )
fucoppc.s ⊢ 𝑆 = ( 𝑂 FuncCat 𝑃 )
fucoppc.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
fucoppc.f ⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
fucoppc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
fucoppc.t ⊢ 𝑇 = ( CatCat ‘ 𝑈 )
fucoppc.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
fucoppc.i ⊢ 𝐼 = ( Iso ‘ 𝑇 )
fucoppc.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
fucoppc.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
fucoppc.1 ⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
fucoppc.2 ⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
Assertion fucoppc ( 𝜑 → 𝐹 ( 𝑅 𝐼 𝑆 ) 𝐺 )

Proof

Step Hyp Ref Expression
1 fucoppc.o ⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2 fucoppc.p ⊢ 𝑃 = ( oppCat ‘ 𝐷 )
3 fucoppc.q ⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
4 fucoppc.r ⊢ 𝑅 = ( oppCat ‘ 𝑄 )
5 fucoppc.s ⊢ 𝑆 = ( 𝑂 FuncCat 𝑃 )
6 fucoppc.n ⊢ 𝑁 = ( 𝐶 Nat 𝐷 )
7 fucoppc.f ⊢ ( 𝜑 → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
8 fucoppc.g ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
9 fucoppc.t ⊢ 𝑇 = ( CatCat ‘ 𝑈 )
10 fucoppc.b ⊢ 𝐵 = ( Base ‘ 𝑇 )
11 fucoppc.i ⊢ 𝐼 = ( Iso ‘ 𝑇 )
12 fucoppc.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
13 fucoppc.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑊 )
14 fucoppc.1 ⊢ ( 𝜑 → 𝑅 ∈ 𝐵 )
15 fucoppc.2 ⊢ ( 𝜑 → 𝑆 ∈ 𝐵 )
16 3 fucbas ⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
17 4 16 oppcbas ⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑅 )
18 5 fucbas ⊢ ( 𝑂 Func 𝑃 ) = ( Base ‘ 𝑆 )
19 eqid ⊢ ( Hom ‘ 𝑅 ) = ( Hom ‘ 𝑅 )
20 eqid ⊢ ( 𝑂 Nat 𝑃 ) = ( 𝑂 Nat 𝑃 )
21 5 20 fuchom ⊢ ( 𝑂 Nat 𝑃 ) = ( Hom ‘ 𝑆 )
22 eqid ⊢ ( Id ‘ 𝑅 ) = ( Id ‘ 𝑅 )
23 eqid ⊢ ( Id ‘ 𝑆 ) = ( Id ‘ 𝑆 )
24 eqid ⊢ ( comp ‘ 𝑅 ) = ( comp ‘ 𝑅 )
25 eqid ⊢ ( comp ‘ 𝑆 ) = ( comp ‘ 𝑆 )
26 9 10 elbasfv ⊢ ( 𝑅 ∈ 𝐵 → 𝑈 ∈ V )
27 14 26 syl ⊢ ( 𝜑 → 𝑈 ∈ V )
28 9 10 27 catcbas ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Cat ) )
29 14 28 eleqtrd ⊢ ( 𝜑 → 𝑅 ∈ ( 𝑈 ∩ Cat ) )
30 29 elin2d ⊢ ( 𝜑 → 𝑅 ∈ Cat )
31 15 28 eleqtrd ⊢ ( 𝜑 → 𝑆 ∈ ( 𝑈 ∩ Cat ) )
32 31 elin2d ⊢ ( 𝜑 → 𝑆 ∈ Cat )
33 1 2 12 13 oppff1o ⊢ ( 𝜑 → ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) )
34 7 f1oeq1d ⊢ ( 𝜑 → ( 𝐹 : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) ↔ ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) ) )
35 33 34 mpbird ⊢ ( 𝜑 → 𝐹 : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) )
36 f1of ⊢ ( 𝐹 : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) → 𝐹 : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) )
37 35 36 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐶 Func 𝐷 ) ⟶ ( 𝑂 Func 𝑃 ) )
38 eqid ⊢ ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) )
39 ovex ⊢ ( 𝑦 𝑁 𝑥 ) ∈ V
40 resiexg ⊢ ( ( 𝑦 𝑁 𝑥 ) ∈ V → ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ∈ V )
41 39 40 ax-mp ⊢ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ∈ V
42 38 41 fnmpoi ⊢ ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) Fn ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) )
43 8 fneq1d ⊢ ( 𝜑 → ( 𝐺 Fn ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) ↔ ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) Fn ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) ) )
44 42 43 mpbiri ⊢ ( 𝜑 → 𝐺 Fn ( ( 𝐶 Func 𝐷 ) × ( 𝐶 Func 𝐷 ) ) )
45 f1oi ⊢ ( I ↾ ( 𝑔 𝑁 𝑓 ) ) : ( 𝑔 𝑁 𝑓 ) –1-1-onto→ ( 𝑔 𝑁 𝑓 )
46 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → 𝐺 = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
47 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
48 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → 𝑔 ∈ ( 𝐶 Func 𝐷 ) )
49 46 47 48 opf2fval ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ( 𝑓 𝐺 𝑔 ) = ( I ↾ ( 𝑔 𝑁 𝑓 ) ) )
50 3 6 fuchom ⊢ 𝑁 = ( Hom ‘ 𝑄 )
51 50 4 oppchom ⊢ ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) = ( 𝑔 𝑁 𝑓 )
52 51 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) = ( 𝑔 𝑁 𝑓 ) )
53 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
54 1 2 6 53 47 48 fucoppclem ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ( 𝑔 𝑁 𝑓 ) = ( ( 𝐹 ‘ 𝑓 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑔 ) ) )
55 54 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ( ( 𝐹 ‘ 𝑓 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑔 ) ) = ( 𝑔 𝑁 𝑓 ) )
56 49 52 55 f1oeq123d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ( ( 𝑓 𝐺 𝑔 ) : ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑓 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑔 ) ) ↔ ( I ↾ ( 𝑔 𝑁 𝑓 ) ) : ( 𝑔 𝑁 𝑓 ) –1-1-onto→ ( 𝑔 𝑁 𝑓 ) ) )
57 45 56 mpbiri ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ( 𝑓 𝐺 𝑔 ) : ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑓 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑔 ) ) )
58 f1of ⊢ ( ( 𝑓 𝐺 𝑔 ) : ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑓 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑔 ) ) → ( 𝑓 𝐺 𝑔 ) : ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) ⟶ ( ( 𝐹 ‘ 𝑓 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑔 ) ) )
59 57 58 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ) ) → ( 𝑓 𝐺 𝑔 ) : ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) ⟶ ( ( 𝐹 ‘ 𝑓 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑔 ) ) )
60 7 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
61 8 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐺 = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
62 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → 𝑓 ∈ ( 𝐶 Func 𝐷 ) )
63 1 2 3 4 5 6 60 61 62 fucoppcid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ) → ( ( 𝑓 𝐺 𝑓 ) ‘ ( ( Id ‘ 𝑅 ) ‘ 𝑓 ) ) = ( ( Id ‘ 𝑆 ) ‘ ( 𝐹 ‘ 𝑓 ) ) )
64 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑘 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑔 ( Hom ‘ 𝑅 ) 𝑘 ) ) ) → 𝐹 = ( oppFunc ↾ ( 𝐶 Func 𝐷 ) ) )
65 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑘 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑔 ( Hom ‘ 𝑅 ) 𝑘 ) ) ) → 𝐺 = ( 𝑥 ∈ ( 𝐶 Func 𝐷 ) , 𝑦 ∈ ( 𝐶 Func 𝐷 ) ↦ ( I ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
66 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑘 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑔 ( Hom ‘ 𝑅 ) 𝑘 ) ) ) → 𝑎 ∈ ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) )
67 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑘 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑔 ( Hom ‘ 𝑅 ) 𝑘 ) ) ) → 𝑏 ∈ ( 𝑔 ( Hom ‘ 𝑅 ) 𝑘 ) )
68 1 2 3 4 5 6 64 65 66 67 fucoppcco ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ∧ 𝑘 ∈ ( 𝐶 Func 𝐷 ) ) ∧ ( 𝑎 ∈ ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) ∧ 𝑏 ∈ ( 𝑔 ( Hom ‘ 𝑅 ) 𝑘 ) ) ) → ( ( 𝑓 𝐺 𝑘 ) ‘ ( 𝑏 ( ⟨ 𝑓 , 𝑔 ⟩ ( comp ‘ 𝑅 ) 𝑘 ) 𝑎 ) ) = ( ( ( 𝑔 𝐺 𝑘 ) ‘ 𝑏 ) ( ⟨ ( 𝐹 ‘ 𝑓 ) , ( 𝐹 ‘ 𝑔 ) ⟩ ( comp ‘ 𝑆 ) ( 𝐹 ‘ 𝑘 ) ) ( ( 𝑓 𝐺 𝑔 ) ‘ 𝑎 ) ) )
69 17 18 19 21 22 23 24 25 30 32 37 44 59 63 68 isfuncd ⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )
70 57 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ( 𝑓 𝐺 𝑔 ) : ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑓 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑔 ) ) )
71 17 19 21 isffth2 ⊢ ( 𝐹 ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) 𝐺 ↔ ( 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 ∧ ∀ 𝑓 ∈ ( 𝐶 Func 𝐷 ) ∀ 𝑔 ∈ ( 𝐶 Func 𝐷 ) ( 𝑓 𝐺 𝑔 ) : ( 𝑓 ( Hom ‘ 𝑅 ) 𝑔 ) –1-1-onto→ ( ( 𝐹 ‘ 𝑓 ) ( 𝑂 Nat 𝑃 ) ( 𝐹 ‘ 𝑔 ) ) ) )
72 69 70 71 sylanbrc ⊢ ( 𝜑 → 𝐹 ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) 𝐺 )
73 df-br ⊢ ( 𝐹 ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) )
74 72 73 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) )
75 69 func1st ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) = 𝐹 )
76 75 f1oeq1d ⊢ ( 𝜑 → ( ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) ↔ 𝐹 : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) ) )
77 35 76 mpbird ⊢ ( 𝜑 → ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) )
78 9 10 17 18 27 14 15 11 catciso ⊢ ( 𝜑 → ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 𝐼 𝑆 ) ↔ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) ∧ ( 1st ‘ ⟨ 𝐹 , 𝐺 ⟩ ) : ( 𝐶 Func 𝐷 ) –1-1-onto→ ( 𝑂 Func 𝑃 ) ) ) )
79 74 77 78 mpbir2and ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 𝐼 𝑆 ) )
80 df-br ⊢ ( 𝐹 ( 𝑅 𝐼 𝑆 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝑅 𝐼 𝑆 ) )
81 79 80 sylibr ⊢ ( 𝜑 → 𝐹 ( 𝑅 𝐼 𝑆 ) 𝐺 )