This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑂 ) )