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 = ( oppCat ` C )
	fucoppc.p	|- P = ( oppCat ` D )
	fucoppc.q	|- Q = ( C FuncCat D )
	fucoppc.r	|- R = ( oppCat ` Q )
	fucoppc.s	|- S = ( O FuncCat P )
	fucoppc.n	|- N = ( C Nat D )
	fucoppc.f	|- ( ph -> F = ( oppFunc |` ( C Func D ) ) )
	fucoppc.g	|- ( ph -> G = ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) )
	fucoppcffth.c	|- ( ph -> C e. Cat )
	fucoppcffth.d	|- ( ph -> D e. Cat )
Assertion	fucoppcfunc	|- ( ph -> F ( R Func S ) G )

Proof

Step	Hyp	Ref	Expression
1		fucoppc.o	|- O = ( oppCat ` C )
2		fucoppc.p	|- P = ( oppCat ` D )
3		fucoppc.q	|- Q = ( C FuncCat D )
4		fucoppc.r	|- R = ( oppCat ` Q )
5		fucoppc.s	|- S = ( O FuncCat P )
6		fucoppc.n	|- N = ( C Nat D )
7		fucoppc.f	|- ( ph -> F = ( oppFunc |` ( C Func D ) ) )
8		fucoppc.g	|- ( ph -> G = ( x e. ( C Func D ) , y e. ( C Func D ) |-> ( _I |` ( y N x ) ) ) )
9		fucoppcffth.c	|- ( ph -> C e. Cat )
10		fucoppcffth.d	|- ( ph -> D e. Cat )
11	1 2 3 4 5 6 7 8 9 10	fucoppcffth	|- ( ph -> F ( ( R Full S ) i^i ( R Faith S ) ) G )
12		inss1	|- ( ( R Full S ) i^i ( R Faith S ) ) C_ ( R Full S )
13		fullfunc	|- ( R Full S ) C_ ( R Func S )
14	12 13	sstri	|- ( ( R Full S ) i^i ( R Faith S ) ) C_ ( R Func S )
15	14	ssbri	|- ( F ( ( R Full S ) i^i ( R Faith S ) ) G -> F ( R Func S ) G )
16	11 15	syl	|- ( ph -> F ( R Func S ) G )