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 ( 𝜑𝐶 = ( 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 ‘ 𝑂 ) )