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 
|- ( 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 ) )