This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑂 ) )