fucoppcffth

Description: A fully faithful 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	fucoppcffth	$⊢ φ \to F ((R Full S) \cap (R Faith 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	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		eqid	$⊢ CatCat (\{R, S\}) = CatCat (\{R, S\})$
12		eqid	$⊢ {Base}_{R} = {Base}_{R}$
13		eqid	$⊢ {Base}_{S} = {Base}_{S}$
14		eqid	$⊢ Iso (CatCat (\{R, S\})) = Iso (CatCat (\{R, S\}))$
15		eqid	$⊢ {Base}_{CatCat (\{R, S\})} = {Base}_{CatCat (\{R, S\})}$
16	3 9 10	fuccat	$⊢ φ \to Q \in Cat$
17	4	oppccat	$⊢ Q \in Cat \to R \in Cat$
18	16 17	syl	$⊢ φ \to R \in Cat$
19		prid1g	$⊢ R \in Cat \to R \in \{R, S\}$
20	18 19	syl	$⊢ φ \to R \in \{R, S\}$
21	20 18	elind	$⊢ φ \to R \in (\{R, S\} \cap Cat)$
22		prex	$⊢ \{R, S\} \in V$
23	22	a1i	$⊢ φ \to \{R, S\} \in V$
24	11 15 23	catcbas	$⊢ φ \to {Base}_{CatCat (\{R, S\})} = \{R, S\} \cap Cat$
25	21 24	eleqtrrd	$⊢ φ \to R \in {Base}_{CatCat (\{R, S\})}$
26	1	oppccat	$⊢ C \in Cat \to O \in Cat$
27	9 26	syl	$⊢ φ \to O \in Cat$
28	2	oppccat	$⊢ D \in Cat \to P \in Cat$
29	10 28	syl	$⊢ φ \to P \in Cat$
30	5 27 29	fuccat	$⊢ φ \to S \in Cat$
31		prid2g	$⊢ S \in Cat \to S \in \{R, S\}$
32	30 31	syl	$⊢ φ \to S \in \{R, S\}$
33	32 30	elind	$⊢ φ \to S \in (\{R, S\} \cap Cat)$
34	33 24	eleqtrrd	$⊢ φ \to S \in {Base}_{CatCat (\{R, S\})}$
35	1 2 3 4 5 6 7 8 11 15 14 9 10 25 34	fucoppc	$⊢ φ \to F (R Iso (CatCat (\{R, S\})) S) G$
36		df-br	$⊢ F (R Iso (CatCat (\{R, S\})) S) G \leftrightarrow ⟨F, G⟩ \in (R Iso (CatCat (\{R, S\})) S)$
37	35 36	sylib	$⊢ φ \to ⟨F, G⟩ \in (R Iso (CatCat (\{R, S\})) S)$
38	11 12 13 14 37	catcisoi	$⊢ φ \to (⟨F, G⟩ \in ((R Full S) \cap (R Faith S)) \land 1^{st} (⟨F, G⟩) : {Base}_{R} \underset{1-1 onto}{⟶} {Base}_{S})$
39	38	simpld	$⊢ φ \to ⟨F, G⟩ \in ((R Full S) \cap (R Faith S))$
40		df-br	$⊢ F ((R Full S) \cap (R Faith S)) G \leftrightarrow ⟨F, G⟩ \in ((R Full S) \cap (R Faith S))$
41	39 40	sylibr	$⊢ φ \to F ((R Full S) \cap (R Faith S)) G$

Metamath Proof Explorer

Theorem fucoppcffth

Proof