fucoppccic

Description: The opposite category of functors is isomorphic to the category of opposite functors. (Contributed by Zhi Wang, 18-Nov-2025)

	Ref	Expression
Hypotheses	fucoppccic.c	$⊢ C = CatCat (U)$
	fucoppccic.b	$⊢ B = {Base}_{C}$
	fucoppccic.x	$⊢ X = oppCat (D FuncCat E)$
	fucoppccic.y	$⊢ Y = oppCat (D) FuncCat oppCat (E)$
	fucoppccic.xb	$⊢ φ \to X \in B$
	fucoppccic.yb	$⊢ φ \to Y \in B$
	fucoppccic.d	$⊢ φ \to D \in V$
	fucoppccic.e	$⊢ φ \to E \in W$
Assertion	fucoppccic	$⊢ φ \to X ≃_{𝑐} (C) Y$

Proof

Step	Hyp	Ref	Expression
1		fucoppccic.c	$⊢ C = CatCat (U)$
2		fucoppccic.b	$⊢ B = {Base}_{C}$
3		fucoppccic.x	$⊢ X = oppCat (D FuncCat E)$
4		fucoppccic.y	$⊢ Y = oppCat (D) FuncCat oppCat (E)$
5		fucoppccic.xb	$⊢ φ \to X \in B$
6		fucoppccic.yb	$⊢ φ \to Y \in B$
7		fucoppccic.d	$⊢ φ \to D \in V$
8		fucoppccic.e	$⊢ φ \to E \in W$
9		eqid	$⊢ Iso (C) = Iso (C)$
10	1 2	elbasfv	$⊢ X \in B \to U \in V$
11	1	catccat	$⊢ U \in V \to C \in Cat$
12	5 10 11	3syl	$⊢ φ \to C \in Cat$
13		eqid	$⊢ oppCat (D) = oppCat (D)$
14		eqid	$⊢ oppCat (E) = oppCat (E)$
15		eqid	$⊢ D FuncCat E = D FuncCat E$
16		eqid	$⊢ D Nat E = D Nat E$
17		eqidd	Could not format ( ph -> ( oppFunc \|` ( D Func E ) ) = ( oppFunc \|` ( D Func E ) ) ) : No typesetting found for \|- ( ph -> ( oppFunc \|` ( D Func E ) ) = ( oppFunc \|` ( D Func E ) ) ) with typecode \|-
18		eqidd	$⊢ φ \to (f \in (D Func E), g \in (D Func E) ⟼ {I ↾}_{(g (D Nat E) f)}) = (f \in (D Func E), g \in (D Func E) ⟼ {I ↾}_{(g (D Nat E) f)})$
19	13 14 15 3 4 16 17 18 1 2 9 7 8 5 6	fucoppc	Could not format ( ph -> ( oppFunc \|` ( D Func E ) ) ( X ( Iso ` C ) Y ) ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) ) : No typesetting found for \|- ( ph -> ( oppFunc \|` ( D Func E ) ) ( X ( Iso ` C ) Y ) ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) ) with typecode \|-
20		df-br	Could not format ( ( oppFunc \|` ( D Func E ) ) ( X ( Iso ` C ) Y ) ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) <-> <. ( oppFunc \|` ( D Func E ) ) , ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) >. e. ( X ( Iso ` C ) Y ) ) : No typesetting found for \|- ( ( oppFunc \|` ( D Func E ) ) ( X ( Iso ` C ) Y ) ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) <-> <. ( oppFunc \|` ( D Func E ) ) , ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) >. e. ( X ( Iso ` C ) Y ) ) with typecode \|-
21	19 20	sylib	Could not format ( ph -> <. ( oppFunc \|` ( D Func E ) ) , ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) >. e. ( X ( Iso ` C ) Y ) ) : No typesetting found for \|- ( ph -> <. ( oppFunc \|` ( D Func E ) ) , ( f e. ( D Func E ) , g e. ( D Func E ) \|-> ( _I \|` ( g ( D Nat E ) f ) ) ) >. e. ( X ( Iso ` C ) Y ) ) with typecode \|-
22	9 2 12 5 6 21	brcici	$⊢ φ \to X ≃_{𝑐} (C) Y$

Metamath Proof Explorer

Theorem fucoppccic

Proof