oppc1stf

Description: The opposite functor of the first projection functor is the first projection functor of opposite categories. (Contributed by Zhi Wang, 19-Nov-2025)

	Ref	Expression
Hypotheses	oppc1stf.o	$⊢ O = oppCat (C)$
	oppc1stf.p	$⊢ P = oppCat (D)$
	oppc1stf.c	$⊢ φ \to C \in V$
	oppc1stf.d	$⊢ φ \to D \in W$
Assertion	oppc1stf	Could not format assertion : No typesetting found for \|- ( ph -> ( oppFunc ` ( C 1stF D ) ) = ( O 1stF P ) ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		oppc1stf.o	$⊢ O = oppCat (C)$
2		oppc1stf.p	$⊢ P = oppCat (D)$
3		oppc1stf.c	$⊢ φ \to C \in V$
4		oppc1stf.d	$⊢ φ \to D \in W$
5		eqid	$⊢ (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (C \times_{c} D) y)}) = (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (C \times_{c} D) y)})$
6	5	tposmpo	$⊢ tpos (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (C \times_{c} D) y)}) = (y \in ({Base}_{C} \times {Base}_{D}), x \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (C \times_{c} D) y)})$
7		eqid	$⊢ Hom (C) = Hom (C)$
8	7 1	oppchom	$⊢ 1^{st} (y) Hom (O) 1^{st} (x) = 1^{st} (x) Hom (C) 1^{st} (y)$
9		eqid	$⊢ Hom (D) = Hom (D)$
10	9 2	oppchom	$⊢ 2^{nd} (y) Hom (P) 2^{nd} (x) = 2^{nd} (x) Hom (D) 2^{nd} (y)$
11	8 10	xpeq12i	$⊢ (1^{st} (y) Hom (O) 1^{st} (x)) \times (2^{nd} (y) Hom (P) 2^{nd} (x)) = (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y))$
12		eqid	$⊢ O \times_{c} P = O \times_{c} P$
13		eqid	$⊢ {Base}_{C} = {Base}_{C}$
14	1 13	oppcbas	$⊢ {Base}_{C} = {Base}_{O}$
15		eqid	$⊢ {Base}_{D} = {Base}_{D}$
16	2 15	oppcbas	$⊢ {Base}_{D} = {Base}_{P}$
17	12 14 16	xpcbas	$⊢ {Base}_{C} \times {Base}_{D} = {Base}_{(O \times_{c} P)}$
18		eqid	$⊢ Hom (O) = Hom (O)$
19		eqid	$⊢ Hom (P) = Hom (P)$
20		eqid	$⊢ Hom (O \times_{c} P) = Hom (O \times_{c} P)$
21		simp2	$⊢ ((φ \land (C \in Cat \land D \in Cat)) \land y \in ({Base}_{C} \times {Base}_{D}) \land x \in ({Base}_{C} \times {Base}_{D})) \to y \in ({Base}_{C} \times {Base}_{D})$
22		simp3	$⊢ ((φ \land (C \in Cat \land D \in Cat)) \land y \in ({Base}_{C} \times {Base}_{D}) \land x \in ({Base}_{C} \times {Base}_{D})) \to x \in ({Base}_{C} \times {Base}_{D})$
23	12 17 18 19 20 21 22	xpchom	$⊢ ((φ \land (C \in Cat \land D \in Cat)) \land y \in ({Base}_{C} \times {Base}_{D}) \land x \in ({Base}_{C} \times {Base}_{D})) \to y Hom (O \times_{c} P) x = (1^{st} (y) Hom (O) 1^{st} (x)) \times (2^{nd} (y) Hom (P) 2^{nd} (x))$
24		eqid	$⊢ C \times_{c} D = C \times_{c} D$
25	24 13 15	xpcbas	$⊢ {Base}_{C} \times {Base}_{D} = {Base}_{(C \times_{c} D)}$
26		eqid	$⊢ Hom (C \times_{c} D) = Hom (C \times_{c} D)$
27	24 25 7 9 26 22 21	xpchom	$⊢ ((φ \land (C \in Cat \land D \in Cat)) \land y \in ({Base}_{C} \times {Base}_{D}) \land x \in ({Base}_{C} \times {Base}_{D})) \to x Hom (C \times_{c} D) y = (1^{st} (x) Hom (C) 1^{st} (y)) \times (2^{nd} (x) Hom (D) 2^{nd} (y))$
28	11 23 27	3eqtr4a	$⊢ ((φ \land (C \in Cat \land D \in Cat)) \land y \in ({Base}_{C} \times {Base}_{D}) \land x \in ({Base}_{C} \times {Base}_{D})) \to y Hom (O \times_{c} P) x = x Hom (C \times_{c} D) y$
29	28	reseq2d	$⊢ ((φ \land (C \in Cat \land D \in Cat)) \land y \in ({Base}_{C} \times {Base}_{D}) \land x \in ({Base}_{C} \times {Base}_{D})) \to {1^{st} ↾}_{(y Hom (O \times_{c} P) x)} = {1^{st} ↾}_{(x Hom (C \times_{c} D) y)}$
30	29	mpoeq3dva	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to (y \in ({Base}_{C} \times {Base}_{D}), x \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(y Hom (O \times_{c} P) x)}) = (y \in ({Base}_{C} \times {Base}_{D}), x \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (C \times_{c} D) y)})$
31	6 30	eqtr4id	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to tpos (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (C \times_{c} D) y)}) = (y \in ({Base}_{C} \times {Base}_{D}), x \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(y Hom (O \times_{c} P) x)})$
32	31	opeq2d	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, tpos (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (C \times_{c} D) y)})⟩ = ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, (y \in ({Base}_{C} \times {Base}_{D}), x \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(y Hom (O \times_{c} P) x)})⟩$
33		simprl	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to C \in Cat$
34		simprr	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to D \in Cat$
35		eqid	$⊢ C {1^{st}}_{F} D = C {1^{st}}_{F} D$
36	24 25 26 33 34 35	1stfval	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to C {1^{st}}_{F} D = ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, (x \in ({Base}_{C} \times {Base}_{D}), y \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(x Hom (C \times_{c} D) y)})⟩$
37	24 33 34 35	1stfcl	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to C {1^{st}}_{F} D \in ((C \times_{c} D) Func C)$
38	36 37	oppfval3	Could not format ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C 1stF D ) ) = <. ( 1st \|` ( ( Base ` C ) X. ( Base ` D ) ) ) , tpos ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) \|-> ( 1st \|` ( x ( Hom ` ( C Xc. D ) ) y ) ) ) >. ) : No typesetting found for \|- ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C 1stF D ) ) = <. ( 1st \|` ( ( Base ` C ) X. ( Base ` D ) ) ) , tpos ( x e. ( ( Base ` C ) X. ( Base ` D ) ) , y e. ( ( Base ` C ) X. ( Base ` D ) ) \|-> ( 1st \|` ( x ( Hom ` ( C Xc. D ) ) y ) ) ) >. ) with typecode \|-
39	1	oppccat	$⊢ C \in Cat \to O \in Cat$
40	33 39	syl	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to O \in Cat$
41	2	oppccat	$⊢ D \in Cat \to P \in Cat$
42	34 41	syl	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to P \in Cat$
43		eqid	$⊢ O {1^{st}}_{F} P = O {1^{st}}_{F} P$
44	12 17 20 40 42 43	1stfval	$⊢ (φ \land (C \in Cat \land D \in Cat)) \to O {1^{st}}_{F} P = ⟨{1^{st} ↾}_{({Base}_{C} \times {Base}_{D})}, (y \in ({Base}_{C} \times {Base}_{D}), x \in ({Base}_{C} \times {Base}_{D}) ⟼ {1^{st} ↾}_{(y Hom (O \times_{c} P) x)})⟩$
45	32 38 44	3eqtr4d	Could not format ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C 1stF D ) ) = ( O 1stF P ) ) : No typesetting found for \|- ( ( ph /\ ( C e. Cat /\ D e. Cat ) ) -> ( oppFunc ` ( C 1stF D ) ) = ( O 1stF P ) ) with typecode \|-
46		df-1stf	$⊢ {1^{st}}_{F} = (c \in Cat, d \in Cat ⟼ ⦋ ({Base}_{c} \times {Base}_{d}) / b ⦌ ⟨{1^{st} ↾}_{b}, (x \in b, y \in b ⟼ {1^{st} ↾}_{(x Hom (c \times_{c} d) y)})⟩)$
47	1 2 3 4 45 46	oppc1stflem	Could not format ( ph -> ( oppFunc ` ( C 1stF D ) ) = ( O 1stF P ) ) : No typesetting found for \|- ( ph -> ( oppFunc ` ( C 1stF D ) ) = ( O 1stF P ) ) with typecode \|-

Metamath Proof Explorer

Theorem oppc1stf

Proof