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