This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fucoppcfunc

Description: A functor from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 19-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 ↾ ( 𝑦 𝑁 𝑥 ) ) ) )
fucoppcffth.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
fucoppcffth.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
Assertion fucoppcfunc ( 𝜑 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )

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 fucoppcffth.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
10 fucoppcffth.d ⊢ ( 𝜑 → 𝐷 ∈ Cat )
11 1 2 3 4 5 6 7 8 9 10 fucoppcffth ⊢ ( 𝜑 → 𝐹 ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) 𝐺 )
12 inss1 ⊢ ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) ⊆ ( 𝑅 Full 𝑆 )
13 fullfunc ⊢ ( 𝑅 Full 𝑆 ) ⊆ ( 𝑅 Func 𝑆 )
14 12 13 sstri ⊢ ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) ⊆ ( 𝑅 Func 𝑆 )
15 14 ssbri ⊢ ( 𝐹 ( ( 𝑅 Full 𝑆 ) ∩ ( 𝑅 Faith 𝑆 ) ) 𝐺 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )
16 11 15 syl ⊢ ( 𝜑 → 𝐹 ( 𝑅 Func 𝑆 ) 𝐺 )