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	$$⊢\phi \to C=\mathrm{ProsetToCat}\left(K\right)$$
	prstcnid.k	$$⊢\phi \to K\in \mathrm{Proset}$$
	oduoppcbas.d	$$⊢\phi \to D=\mathrm{ProsetToCat}\left(\mathrm{ODual}\left(K\right)\right)$$
	oduoppcbas.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
Assertion	oduoppcbas	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_O$$

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	$$⊢\phi \to C=\mathrm{ProsetToCat}\left(K\right)$$
2		prstcnid.k	$$⊢\phi \to K\in \mathrm{Proset}$$
3		oduoppcbas.d	$$⊢\phi \to D=\mathrm{ProsetToCat}\left(\mathrm{ODual}\left(K\right)\right)$$
4		oduoppcbas.o	$$⊢O=\mathrm{oppCat}\left(C\right)$$
5		eqid	$$⊢\mathrm{ODual}\left(K\right)=\mathrm{ODual}\left(K\right)$$
6	5	oduprs	$$⊢K\in \mathrm{Proset}\to \mathrm{ODual}\left(K\right)\in \mathrm{Proset}$$
7	2 6	syl	$$⊢\phi \to \mathrm{ODual}\left(K\right)\in \mathrm{Proset}$$
8		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
9	5 8	odubas	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{ODual}\left(K\right)}$$
10	9	a1i	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_{\mathrm{ODual}\left(K\right)}$$
11	3 7 10	prstcbas	$$⊢\phi \to {\mathrm{Base}}_K={\mathrm{Base}}_D$$
12	11	eqcomd	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_K$$
13	1 2 12	prstcbas	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_C$$
14		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
15	4 14	oppcbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_O$$
16	13 15	eqtrdi	$$⊢\phi \to {\mathrm{Base}}_D={\mathrm{Base}}_O$$