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	|- ( ph -> C = ( ProsetToCat ` K ) )
	prstcnid.k	|- ( ph -> K e. Proset )
	oduoppcbas.d	|- ( ph -> D = ( ProsetToCat ` ( ODual ` K ) ) )
	oduoppcbas.o	|- O = ( oppCat ` C )
Assertion	oduoppcbas	|- ( ph -> ( Base ` D ) = ( Base ` O ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
2		prstcnid.k	|- ( ph -> K e. Proset )
3		oduoppcbas.d	|- ( ph -> D = ( ProsetToCat ` ( ODual ` K ) ) )
4		oduoppcbas.o	|- O = ( oppCat ` C )
5		eqid	|- ( ODual ` K ) = ( ODual ` K )
6	5	oduprs	|- ( K e. Proset -> ( ODual ` K ) e. Proset )
7	2 6	syl	|- ( ph -> ( ODual ` K ) e. Proset )
8		eqid	|- ( Base ` K ) = ( Base ` K )
9	5 8	odubas	|- ( Base ` K ) = ( Base ` ( ODual ` K ) )
10	9	a1i	|- ( ph -> ( Base ` K ) = ( Base ` ( ODual ` K ) ) )
11	3 7 10	prstcbas	|- ( ph -> ( Base ` K ) = ( Base ` D ) )
12	11	eqcomd	|- ( ph -> ( Base ` D ) = ( Base ` K ) )
13	1 2 12	prstcbas	|- ( ph -> ( Base ` D ) = ( Base ` C ) )
14		eqid	|- ( Base ` C ) = ( Base ` C )
15	4 14	oppcbas	|- ( Base ` C ) = ( Base ` O )
16	13 15	eqtrdi	|- ( ph -> ( Base ` D ) = ( Base ` O ) )