fucoppc

Description: The isomorphism from the opposite category of functors to the category of opposite functors. (Contributed by Zhi Wang, 18-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)})$
	fucoppc.t	$⊢ T = CatCat (U)$
	fucoppc.b	$⊢ B = {Base}_{T}$
	fucoppc.i	$⊢ I = Iso (T)$
	fucoppc.c	$⊢ φ \to C \in V$
	fucoppc.d	$⊢ φ \to D \in W$
	fucoppc.1	$⊢ φ \to R \in B$
	fucoppc.2	$⊢ φ \to S \in B$
Assertion	fucoppc	$⊢ φ \to F (R I 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		fucoppc.t	$⊢ T = CatCat (U)$
10		fucoppc.b	$⊢ B = {Base}_{T}$
11		fucoppc.i	$⊢ I = Iso (T)$
12		fucoppc.c	$⊢ φ \to C \in V$
13		fucoppc.d	$⊢ φ \to D \in W$
14		fucoppc.1	$⊢ φ \to R \in B$
15		fucoppc.2	$⊢ φ \to S \in B$
16	3	fucbas	$⊢ C Func D = {Base}_{Q}$
17	4 16	oppcbas	$⊢ C Func D = {Base}_{R}$
18	5	fucbas	$⊢ O Func P = {Base}_{S}$
19		eqid	$⊢ Hom (R) = Hom (R)$
20		eqid	$⊢ O Nat P = O Nat P$
21	5 20	fuchom	$⊢ O Nat P = Hom (S)$
22		eqid	$⊢ Id (R) = Id (R)$
23		eqid	$⊢ Id (S) = Id (S)$
24		eqid	$⊢ comp (R) = comp (R)$
25		eqid	$⊢ comp (S) = comp (S)$
26	9 10	elbasfv	$⊢ R \in B \to U \in V$
27	14 26	syl	$⊢ φ \to U \in V$
28	9 10 27	catcbas	$⊢ φ \to B = U \cap Cat$
29	14 28	eleqtrd	$⊢ φ \to R \in (U \cap Cat)$
30	29	elin2d	$⊢ φ \to R \in Cat$
31	15 28	eleqtrd	$⊢ φ \to S \in (U \cap Cat)$
32	31	elin2d	$⊢ φ \to S \in Cat$
33	1 2 12 13	oppff1o	Could not format ( ph -> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) ) : No typesetting found for \|- ( ph -> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) ) with typecode \|-
34	7	f1oeq1d	Could not format ( ph -> ( F : ( C Func D ) -1-1-onto-> ( O Func P ) <-> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) ) ) : No typesetting found for \|- ( ph -> ( F : ( C Func D ) -1-1-onto-> ( O Func P ) <-> ( oppFunc \|` ( C Func D ) ) : ( C Func D ) -1-1-onto-> ( O Func P ) ) ) with typecode \|-
35	33 34	mpbird	$⊢ φ \to F : C Func D \underset{1-1 onto}{⟶} O Func P$
36		f1of	$⊢ F : C Func D \underset{1-1 onto}{⟶} O Func P \to F : C Func D ⟶ O Func P$
37	35 36	syl	$⊢ φ \to F : C Func D ⟶ O Func P$
38		eqid	$⊢ (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)}) = (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)})$
39		ovex	$⊢ y N x \in V$
40		resiexg	$⊢ y N x \in V \to {I ↾}_{(y N x)} \in V$
41	39 40	ax-mp	$⊢ {I ↾}_{(y N x)} \in V$
42	38 41	fnmpoi	$⊢ (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)}) Fn ((C Func D) \times (C Func D))$
43	8	fneq1d	$⊢ φ \to (G Fn ((C Func D) \times (C Func D)) \leftrightarrow (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)}) Fn ((C Func D) \times (C Func D)))$
44	42 43	mpbiri	$⊢ φ \to G Fn ((C Func D) \times (C Func D))$
45		f1oi	$⊢ ({I ↾}_{(g N f)}) : g N f \underset{1-1 onto}{⟶} g N f$
46	8	adantr	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to G = (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)})$
47		simprl	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to f \in (C Func D)$
48		simprr	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to g \in (C Func D)$
49	46 47 48	opf2fval	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to f G g = {I ↾}_{(g N f)}$
50	3 6	fuchom	$⊢ N = Hom (Q)$
51	50 4	oppchom	$⊢ f Hom (R) g = g N f$
52	51	a1i	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to f Hom (R) g = g N f$
53	7	adantr	Could not format ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> F = ( oppFunc \|` ( C Func D ) ) ) : No typesetting found for \|- ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) ) ) -> F = ( oppFunc \|` ( C Func D ) ) ) with typecode \|-
54	1 2 6 53 47 48	fucoppclem	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to g N f = F (f) (O Nat P) F (g)$
55	54	eqcomd	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to F (f) (O Nat P) F (g) = g N f$
56	49 52 55	f1oeq123d	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to ((f G g) : f Hom (R) g \underset{1-1 onto}{⟶} F (f) (O Nat P) F (g) \leftrightarrow ({I ↾}_{(g N f)}) : g N f \underset{1-1 onto}{⟶} g N f)$
57	45 56	mpbiri	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to (f G g) : f Hom (R) g \underset{1-1 onto}{⟶} F (f) (O Nat P) F (g)$
58		f1of	$⊢ (f G g) : f Hom (R) g \underset{1-1 onto}{⟶} F (f) (O Nat P) F (g) \to (f G g) : f Hom (R) g ⟶ F (f) (O Nat P) F (g)$
59	57 58	syl	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D))) \to (f G g) : f Hom (R) g ⟶ F (f) (O Nat P) F (g)$
60	7	adantr	Could not format ( ( ph /\ f e. ( C Func D ) ) -> F = ( oppFunc \|` ( C Func D ) ) ) : No typesetting found for \|- ( ( ph /\ f e. ( C Func D ) ) -> F = ( oppFunc \|` ( C Func D ) ) ) with typecode \|-
61	8	adantr	$⊢ (φ \land f \in (C Func D)) \to G = (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)})$
62		simpr	$⊢ (φ \land f \in (C Func D)) \to f \in (C Func D)$
63	1 2 3 4 5 6 60 61 62	fucoppcid	$⊢ (φ \land f \in (C Func D)) \to (f G f) (Id (R) (f)) = Id (S) (F (f))$
64	7	3ad2ant1	Could not format ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) /\ k e. ( C Func D ) ) /\ ( a e. ( f ( Hom ` R ) g ) /\ b e. ( g ( Hom ` R ) k ) ) ) -> F = ( oppFunc \|` ( C Func D ) ) ) : No typesetting found for \|- ( ( ph /\ ( f e. ( C Func D ) /\ g e. ( C Func D ) /\ k e. ( C Func D ) ) /\ ( a e. ( f ( Hom ` R ) g ) /\ b e. ( g ( Hom ` R ) k ) ) ) -> F = ( oppFunc \|` ( C Func D ) ) ) with typecode \|-
65	8	3ad2ant1	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D) \land k \in (C Func D)) \land (a \in (f Hom (R) g) \land b \in (g Hom (R) k))) \to G = (x \in (C Func D), y \in (C Func D) ⟼ {I ↾}_{(y N x)})$
66		simp3l	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D) \land k \in (C Func D)) \land (a \in (f Hom (R) g) \land b \in (g Hom (R) k))) \to a \in (f Hom (R) g)$
67		simp3r	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D) \land k \in (C Func D)) \land (a \in (f Hom (R) g) \land b \in (g Hom (R) k))) \to b \in (g Hom (R) k)$
68	1 2 3 4 5 6 64 65 66 67	fucoppcco	$⊢ (φ \land (f \in (C Func D) \land g \in (C Func D) \land k \in (C Func D)) \land (a \in (f Hom (R) g) \land b \in (g Hom (R) k))) \to (f G k) (b (⟨f, g⟩ comp (R) k) a) = (g G k) (b) (⟨F (f), F (g)⟩ comp (S) F (k)) (f G g) (a)$
69	17 18 19 21 22 23 24 25 30 32 37 44 59 63 68	isfuncd	$⊢ φ \to F (R Func S) G$
70	57	ralrimivva	$⊢ φ \to \forall f \in (C Func D) \forall g \in (C Func D) (f G g) : f Hom (R) g \underset{1-1 onto}{⟶} F (f) (O Nat P) F (g)$
71	17 19 21	isffth2	$⊢ F ((R Full S) \cap (R Faith S)) G \leftrightarrow (F (R Func S) G \land \forall f \in (C Func D) \forall g \in (C Func D) (f G g) : f Hom (R) g \underset{1-1 onto}{⟶} F (f) (O Nat P) F (g))$
72	69 70 71	sylanbrc	$⊢ φ \to F ((R Full S) \cap (R Faith S)) G$
73		df-br	$⊢ F ((R Full S) \cap (R Faith S)) G \leftrightarrow ⟨F, G⟩ \in ((R Full S) \cap (R Faith S))$
74	72 73	sylib	$⊢ φ \to ⟨F, G⟩ \in ((R Full S) \cap (R Faith S))$
75	69	func1st	$⊢ φ \to 1^{st} (⟨F, G⟩) = F$
76	75	f1oeq1d	$⊢ φ \to (1^{st} (⟨F, G⟩) : C Func D \underset{1-1 onto}{⟶} O Func P \leftrightarrow F : C Func D \underset{1-1 onto}{⟶} O Func P)$
77	35 76	mpbird	$⊢ φ \to 1^{st} (⟨F, G⟩) : C Func D \underset{1-1 onto}{⟶} O Func P$
78	9 10 17 18 27 14 15 11	catciso	$⊢ φ \to (⟨F, G⟩ \in (R I S) \leftrightarrow (⟨F, G⟩ \in ((R Full S) \cap (R Faith S)) \land 1^{st} (⟨F, G⟩) : C Func D \underset{1-1 onto}{⟶} O Func P))$
79	74 77 78	mpbir2and	$⊢ φ \to ⟨F, G⟩ \in (R I S)$
80		df-br	$⊢ F (R I S) G \leftrightarrow ⟨F, G⟩ \in (R I S)$
81	79 80	sylibr	$⊢ φ \to F (R I S) G$

Metamath Proof Explorer

Theorem fucoppc

Proof