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	No typesetting found for \|- ( ph -> F = ( oppFunc \|` ( C Func D ) ) ) with typecode \|-
	fucoppc.g	$⊢ φ \to G = (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)})$
	fucoppcffth.c	$⊢ φ \to C \in Cat$
	fucoppcffth.d	$⊢ φ \to D \in Cat$
Assertion	fucoppcfunc	$⊢ φ \to F (R Func S) G$

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	Could not format ( ph -> F = ( oppFunc \|` ( C Func D ) ) ) : No typesetting found for \|- ( ph -> F = ( oppFunc \|` ( C Func D ) ) ) with typecode \|-
8		fucoppc.g	$⊢ φ \to G = (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)})$
9		fucoppcffth.c	$⊢ φ \to C \in Cat$
10		fucoppcffth.d	$⊢ φ \to D \in Cat$
11	1 2 3 4 5 6 7 8 9 10	fucoppcffth	$⊢ φ \to F ((R Full S) \cap (R Faith S)) G$
12		inss1	$⊢ (R Full S) \cap (R Faith S) \subseteq R Full S$
13		fullfunc	$⊢ R Full S \subseteq R Func S$
14	12 13	sstri	$⊢ (R Full S) \cap (R Faith S) \subseteq R Func S$
15	14	ssbri	$⊢ F ((R Full S) \cap (R Faith S)) G \to F (R Func S) G$
16	11 15	syl	$⊢ φ \to F (R Func S) G$

Metamath Proof Explorer