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

Metamath Proof Explorer

Theorem oduoppcbas

Description: The dual of a preordered set and the opposite category have the same set of objects. (Contributed by Zhi Wang, 22-Sep-2025)

Ref Expression
Hypotheses prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
oduoppcbas.d ⊢ φ → D = ProsetToCat ⁡ ODual ⁡ K
oduoppcbas.o ⊢ O = oppCat ⁡ C
Assertion oduoppcbas ⊢ φ → Base D = Base O

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
2 prstcnid.k ⊢ φ → K ∈ Proset
3 oduoppcbas.d ⊢ φ → D = ProsetToCat ⁡ ODual ⁡ K
4 oduoppcbas.o ⊢ O = oppCat ⁡ C
5 eqid ⊢ ODual ⁡ K = ODual ⁡ K
6 5 oduprs ⊢ K ∈ Proset → ODual ⁡ K ∈ Proset
7 2 6 syl ⊢ φ → ODual ⁡ K ∈ Proset
8 eqid ⊢ Base K = Base K
9 5 8 odubas ⊢ Base K = Base ODual ⁡ K
10 9 a1i ⊢ φ → Base K = Base ODual ⁡ K
11 3 7 10 prstcbas ⊢ φ → Base K = Base D
12 11 eqcomd ⊢ φ → Base D = Base K
13 1 2 12 prstcbas ⊢ φ → Base D = Base C
14 eqid ⊢ Base C = Base C
15 4 14 oppcbas ⊢ Base C = Base O
16 13 15 eqtrdi ⊢ φ → Base D = Base O