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 𝑆 ) 𝐺 )