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	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	oduoppcbas.d	⊢ ( 𝜑 → 𝐷 = ( ProsetToCat ‘ ( ODual ‘ 𝐾 ) ) )
	oduoppcbas.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
Assertion	oduoppcbas	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝑂 ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3		oduoppcbas.d	⊢ ( 𝜑 → 𝐷 = ( ProsetToCat ‘ ( ODual ‘ 𝐾 ) ) )
4		oduoppcbas.o	⊢ 𝑂 = ( oppCat ‘ 𝐶 )
5		eqid	⊢ ( ODual ‘ 𝐾 ) = ( ODual ‘ 𝐾 )
6	5	oduprs	⊢ ( 𝐾 ∈ Proset → ( ODual ‘ 𝐾 ) ∈ Proset )
7	2 6	syl	⊢ ( 𝜑 → ( ODual ‘ 𝐾 ) ∈ Proset )
8		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
9	5 8	odubas	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ ( ODual ‘ 𝐾 ) )
10	9	a1i	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ ( ODual ‘ 𝐾 ) ) )
11	3 7 10	prstcbas	⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐷 ) )
12	11	eqcomd	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐾 ) )
13	1 2 12	prstcbas	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝐶 ) )
14		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
15	4 14	oppcbas	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝑂 )
16	13 15	eqtrdi	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = ( Base ‘ 𝑂 ) )