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	$$⊢O=\mathrm{oppCat}\left(C\right)$$
	fucoppc.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
	fucoppc.q	$$⊢Q=C\mathrm{FuncCat}D$$
	fucoppc.r	$$⊢R=\mathrm{oppCat}\left(Q\right)$$
	fucoppc.s	$$⊢S=O\mathrm{FuncCat}P$$
	fucoppc.n	$$⊢N=C\mathrm{Nat}D$$
	fucoppc.f	No typesetting found for |- ( ph -> F = ( oppFunc |` ( C Func D ) ) ) with typecode |-
	fucoppc.g	$$⊢\phi \to G=\left(x\in \left(C\mathrm{Func}D\right),y\in \left(C\mathrm{Func}D\right)⟼{\mathrm{I}\upharpoonright }_{\left(yNx\right)}\right)$$
	fucoppcffth.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	fucoppcffth.d	$$⊢\phi \to D\in \mathrm{Cat}$$
Assertion	fucoppcfunc	$$⊢\phi \to F\left(R\mathrm{Func}S\right)G$$

Proof

Step	Hyp	Ref	Expression
1		fucoppc.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
2		fucoppc.p	$$⊢P=\mathrm{oppCat}\left(D\right)$$
3		fucoppc.q	$$⊢Q=C\mathrm{FuncCat}D$$
4		fucoppc.r	$$⊢R=\mathrm{oppCat}\left(Q\right)$$
5		fucoppc.s	$$⊢S=O\mathrm{FuncCat}P$$
6		fucoppc.n	$$⊢N=C\mathrm{Nat}D$$
7		fucoppc.f	Could not format ( ph -> F = ( oppFunc |` ( C Func D ) ) ) : No typesetting found for |- ( ph -> F = ( oppFunc |` ( C Func D ) ) ) with typecode |-
8		fucoppc.g	$$⊢\phi \to G=\left(x\in \left(C\mathrm{Func}D\right),y\in \left(C\mathrm{Func}D\right)⟼{\mathrm{I}\upharpoonright }_{\left(yNx\right)}\right)$$
9		fucoppcffth.c	$$⊢\phi \to C\in \mathrm{Cat}$$
10		fucoppcffth.d	$$⊢\phi \to D\in \mathrm{Cat}$$
11	1 2 3 4 5 6 7 8 9 10	fucoppcffth	$$⊢\phi \to F\left(\left(R\mathrm{Full}S\right)\cap \left(R\mathrm{Faith}S\right)\right)G$$
12		inss1	$$⊢\left(R\mathrm{Full}S\right)\cap \left(R\mathrm{Faith}S\right)\subseteq R\mathrm{Full}S$$
13		fullfunc	$$⊢R\mathrm{Full}S\subseteq R\mathrm{Func}S$$
14	12 13	sstri	$$⊢\left(R\mathrm{Full}S\right)\cap \left(R\mathrm{Faith}S\right)\subseteq R\mathrm{Func}S$$
15	14	ssbri	$$⊢F\left(\left(R\mathrm{Full}S\right)\cap \left(R\mathrm{Faith}S\right)\right)G\to F\left(R\mathrm{Func}S\right)G$$
16	11 15	syl	$$⊢\phi \to F\left(R\mathrm{Func}S\right)G$$