Theorem 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	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
	oppcendc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	oppcendc.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	oppcendc.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
Assertion	oppcendc	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		oppcendc.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
2		oppcendc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		oppcendc.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		oppcendc.1	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
5	4	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
6		eqeq12	⊢ ( ( 𝑥 = 𝑝 ∧ 𝑦 = 𝑞 ) → ( 𝑥 = 𝑦 ↔ 𝑝 = 𝑞 ) )
7	6	necon3bid	⊢ ( ( 𝑥 = 𝑝 ∧ 𝑦 = 𝑞 ) → ( 𝑥 ≠ 𝑦 ↔ 𝑝 ≠ 𝑞 ) )
8		oveq12	⊢ ( ( 𝑥 = 𝑝 ∧ 𝑦 = 𝑞 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑝 𝐻 𝑞 ) )
9	8	eqeq1d	⊢ ( ( 𝑥 = 𝑝 ∧ 𝑦 = 𝑞 ) → ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( 𝑝 𝐻 𝑞 ) = ∅ ) )
10	7 9	imbi12d	⊢ ( ( 𝑥 = 𝑝 ∧ 𝑦 = 𝑞 ) → ( ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) ↔ ( 𝑝 ≠ 𝑞 → ( 𝑝 𝐻 𝑞 ) = ∅ ) ) )
11	10	rspc2gv	⊢ ( ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( 𝑝 ≠ 𝑞 → ( 𝑝 𝐻 𝑞 ) = ∅ ) ) )
12	5 11	mpan9	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 ≠ 𝑞 → ( 𝑝 𝐻 𝑞 ) = ∅ ) )
13		simprr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → 𝑞 ∈ 𝐵 )
14		simprl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → 𝑝 ∈ 𝐵 )
15	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) )
16		eqeq12	⊢ ( ( 𝑥 = 𝑞 ∧ 𝑦 = 𝑝 ) → ( 𝑥 = 𝑦 ↔ 𝑞 = 𝑝 ) )
17		equcom	⊢ ( 𝑝 = 𝑞 ↔ 𝑞 = 𝑝 )
18	16 17	bitr4di	⊢ ( ( 𝑥 = 𝑞 ∧ 𝑦 = 𝑝 ) → ( 𝑥 = 𝑦 ↔ 𝑝 = 𝑞 ) )
19	18	necon3bid	⊢ ( ( 𝑥 = 𝑞 ∧ 𝑦 = 𝑝 ) → ( 𝑥 ≠ 𝑦 ↔ 𝑝 ≠ 𝑞 ) )
20		oveq12	⊢ ( ( 𝑥 = 𝑞 ∧ 𝑦 = 𝑝 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑞 𝐻 𝑝 ) )
21	20	eqeq1d	⊢ ( ( 𝑥 = 𝑞 ∧ 𝑦 = 𝑝 ) → ( ( 𝑥 𝐻 𝑦 ) = ∅ ↔ ( 𝑞 𝐻 𝑝 ) = ∅ ) )
22	19 21	imbi12d	⊢ ( ( 𝑥 = 𝑞 ∧ 𝑦 = 𝑝 ) → ( ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) ↔ ( 𝑝 ≠ 𝑞 → ( 𝑞 𝐻 𝑝 ) = ∅ ) ) )
23	22	rspc2gv	⊢ ( ( 𝑞 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) → ( 𝑝 ≠ 𝑞 → ( 𝑞 𝐻 𝑝 ) = ∅ ) ) )
24	23	imp	⊢ ( ( ( 𝑞 ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ≠ 𝑦 → ( 𝑥 𝐻 𝑦 ) = ∅ ) ) → ( 𝑝 ≠ 𝑞 → ( 𝑞 𝐻 𝑝 ) = ∅ ) )
25	13 14 15 24	syl21anc	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 ≠ 𝑞 → ( 𝑞 𝐻 𝑝 ) = ∅ ) )
26	12 25	jcad	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 ≠ 𝑞 → ( ( 𝑝 𝐻 𝑞 ) = ∅ ∧ ( 𝑞 𝐻 𝑝 ) = ∅ ) ) )
27		nne	⊢ ( ¬ 𝑝 ≠ 𝑞 ↔ 𝑝 = 𝑞 )
28		id	⊢ ( 𝑝 = 𝑞 → 𝑝 = 𝑞 )
29		equcomi	⊢ ( 𝑝 = 𝑞 → 𝑞 = 𝑝 )
30	28 29	oveq12d	⊢ ( 𝑝 = 𝑞 → ( 𝑝 𝐻 𝑞 ) = ( 𝑞 𝐻 𝑝 ) )
31	27 30	sylbi	⊢ ( ¬ 𝑝 ≠ 𝑞 → ( 𝑝 𝐻 𝑞 ) = ( 𝑞 𝐻 𝑝 ) )
32		eqtr3	⊢ ( ( ( 𝑝 𝐻 𝑞 ) = ∅ ∧ ( 𝑞 𝐻 𝑝 ) = ∅ ) → ( 𝑝 𝐻 𝑞 ) = ( 𝑞 𝐻 𝑝 ) )
33	31 32	ja	⊢ ( ( 𝑝 ≠ 𝑞 → ( ( 𝑝 𝐻 𝑞 ) = ∅ ∧ ( 𝑞 𝐻 𝑝 ) = ∅ ) ) → ( 𝑝 𝐻 𝑞 ) = ( 𝑞 𝐻 𝑝 ) )
34	26 33	syl	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 𝐻 𝑞 ) = ( 𝑞 𝐻 𝑝 ) )
35		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
36	35 2 3 14 13	homfval	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 ( Homf ‘ 𝐶 ) 𝑞 ) = ( 𝑝 𝐻 𝑞 ) )
37	35 2 3 13 14	homfval	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑞 ( Homf ‘ 𝐶 ) 𝑝 ) = ( 𝑞 𝐻 𝑝 ) )
38	34 36 37	3eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵 ) ) → ( 𝑝 ( Homf ‘ 𝐶 ) 𝑞 ) = ( 𝑞 ( Homf ‘ 𝐶 ) 𝑝 ) )
39	38	ralrimivva	⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝐵 ∀ 𝑞 ∈ 𝐵 ( 𝑝 ( Homf ‘ 𝐶 ) 𝑞 ) = ( 𝑞 ( Homf ‘ 𝐶 ) 𝑝 ) )
40	35 2	homffn	⊢ ( Homf ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 )
41		tpossym	⊢ ( ( Homf ‘ 𝐶 ) Fn ( 𝐵 × 𝐵 ) → ( tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 ) ↔ ∀ 𝑝 ∈ 𝐵 ∀ 𝑞 ∈ 𝐵 ( 𝑝 ( Homf ‘ 𝐶 ) 𝑞 ) = ( 𝑞 ( Homf ‘ 𝐶 ) 𝑝 ) ) )
42	40 41	ax-mp	⊢ ( tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 ) ↔ ∀ 𝑝 ∈ 𝐵 ∀ 𝑞 ∈ 𝐵 ( 𝑝 ( Homf ‘ 𝐶 ) 𝑞 ) = ( 𝑞 ( Homf ‘ 𝐶 ) 𝑝 ) )
43	39 42	sylibr	⊢ ( 𝜑 → tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 ) )
44	1 35	oppchomf	⊢ tpos ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 )
45	43 44	eqtr3di	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝑂 ) )