oppcendc

Description: The opposite category of a category whose morphisms are all endomorphisms has the same base and hom-sets as the original category. (Contributed by Zhi Wang, 16-Oct-2025)

	Ref	Expression
Hypotheses	oppcendc.o	$⊢ O = oppCat (C)$
	oppcendc.b	$⊢ B = {Base}_{C}$
	oppcendc.h	$⊢ H = Hom (C)$
	oppcendc.1	$⊢ (φ \land (x \in B \land y \in B)) \to (x \neq y \to x H y = \emptyset)$
Assertion	oppcendc	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$

Proof

Step	Hyp	Ref	Expression
1		oppcendc.o	$⊢ O = oppCat (C)$
2		oppcendc.b	$⊢ B = {Base}_{C}$
3		oppcendc.h	$⊢ H = Hom (C)$
4		oppcendc.1	$⊢ (φ \land (x \in B \land y \in B)) \to (x \neq y \to x H y = \emptyset)$
5	4	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B (x \neq y \to x H y = \emptyset)$
6		eqeq12	$⊢ (x = p \land y = q) \to (x = y \leftrightarrow p = q)$
7	6	necon3bid	$⊢ (x = p \land y = q) \to (x \neq y \leftrightarrow p \neq q)$
8		oveq12	$⊢ (x = p \land y = q) \to x H y = p H q$
9	8	eqeq1d	$⊢ (x = p \land y = q) \to (x H y = \emptyset \leftrightarrow p H q = \emptyset)$
10	7 9	imbi12d	$⊢ (x = p \land y = q) \to ((x \neq y \to x H y = \emptyset) \leftrightarrow (p \neq q \to p H q = \emptyset))$
11	10	rspc2gv	$⊢ (p \in B \land q \in B) \to (\forall x \in B \forall y \in B (x \neq y \to x H y = \emptyset) \to (p \neq q \to p H q = \emptyset))$
12	5 11	mpan9	$⊢ (φ \land (p \in B \land q \in B)) \to (p \neq q \to p H q = \emptyset)$
13		simprr	$⊢ (φ \land (p \in B \land q \in B)) \to q \in B$
14		simprl	$⊢ (φ \land (p \in B \land q \in B)) \to p \in B$
15	5	adantr	$⊢ (φ \land (p \in B \land q \in B)) \to \forall x \in B \forall y \in B (x \neq y \to x H y = \emptyset)$
16		eqeq12	$⊢ (x = q \land y = p) \to (x = y \leftrightarrow q = p)$
17		equcom	$⊢ p = q \leftrightarrow q = p$
18	16 17	bitr4di	$⊢ (x = q \land y = p) \to (x = y \leftrightarrow p = q)$
19	18	necon3bid	$⊢ (x = q \land y = p) \to (x \neq y \leftrightarrow p \neq q)$
20		oveq12	$⊢ (x = q \land y = p) \to x H y = q H p$
21	20	eqeq1d	$⊢ (x = q \land y = p) \to (x H y = \emptyset \leftrightarrow q H p = \emptyset)$
22	19 21	imbi12d	$⊢ (x = q \land y = p) \to ((x \neq y \to x H y = \emptyset) \leftrightarrow (p \neq q \to q H p = \emptyset))$
23	22	rspc2gv	$⊢ (q \in B \land p \in B) \to (\forall x \in B \forall y \in B (x \neq y \to x H y = \emptyset) \to (p \neq q \to q H p = \emptyset))$
24	23	imp	$⊢ ((q \in B \land p \in B) \land \forall x \in B \forall y \in B (x \neq y \to x H y = \emptyset)) \to (p \neq q \to q H p = \emptyset)$
25	13 14 15 24	syl21anc	$⊢ (φ \land (p \in B \land q \in B)) \to (p \neq q \to q H p = \emptyset)$
26	12 25	jcad	$⊢ (φ \land (p \in B \land q \in B)) \to (p \neq q \to (p H q = \emptyset \land q H p = \emptyset))$
27		nne	$⊢ \neg p \neq q \leftrightarrow p = q$
28		id	$⊢ p = q \to p = q$
29		equcomi	$⊢ p = q \to q = p$
30	28 29	oveq12d	$⊢ p = q \to p H q = q H p$
31	27 30	sylbi	$⊢ \neg p \neq q \to p H q = q H p$
32		eqtr3	$⊢ (p H q = \emptyset \land q H p = \emptyset) \to p H q = q H p$
33	31 32	ja	$⊢ (p \neq q \to (p H q = \emptyset \land q H p = \emptyset)) \to p H q = q H p$
34	26 33	syl	$⊢ (φ \land (p \in B \land q \in B)) \to p H q = q H p$
35		eqid	$⊢ {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
36	35 2 3 14 13	homfval	$⊢ (φ \land (p \in B \land q \in B)) \to p {Hom}_{𝑓} (C) q = p H q$
37	35 2 3 13 14	homfval	$⊢ (φ \land (p \in B \land q \in B)) \to q {Hom}_{𝑓} (C) p = q H p$
38	34 36 37	3eqtr4d	$⊢ (φ \land (p \in B \land q \in B)) \to p {Hom}_{𝑓} (C) q = q {Hom}_{𝑓} (C) p$
39	38	ralrimivva	$⊢ φ \to \forall p \in B \forall q \in B p {Hom}_{𝑓} (C) q = q {Hom}_{𝑓} (C) p$
40	35 2	homffn	$⊢ {Hom}_{𝑓} (C) Fn (B \times B)$
41		tpossym	$⊢ {Hom}_{𝑓} (C) Fn (B \times B) \to (tpos {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C) \leftrightarrow \forall p \in B \forall q \in B p {Hom}_{𝑓} (C) q = q {Hom}_{𝑓} (C) p)$
42	40 41	ax-mp	$⊢ tpos {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C) \leftrightarrow \forall p \in B \forall q \in B p {Hom}_{𝑓} (C) q = q {Hom}_{𝑓} (C) p$
43	39 42	sylibr	$⊢ φ \to tpos {Hom}_{𝑓} (C) = {Hom}_{𝑓} (C)$
44	1 35	oppchomf	$⊢ tpos {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$
45	43 44	eqtr3di	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (O)$

Metamath Proof Explorer

Theorem oppcendc

Proof