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

Metamath Proof Explorer

Theorem odubas

Description: Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015) (Proof shortened by AV, 12-Nov-2024)

Ref Expression
Hypotheses oduval.d 
|- D = ( ODual ` O )
odubas.b 
|- B = ( Base ` O )
Assertion odubas 
|- B = ( Base ` D )

Proof

Step Hyp Ref Expression
1 oduval.d 
 |-  D = ( ODual ` O )
2 odubas.b 
 |-  B = ( Base ` O )
3 baseid 
 |-  Base = Slot ( Base ` ndx )
4 plendxnbasendx 
 |-  ( le ` ndx ) =/= ( Base ` ndx )
5 4 necomi 
 |-  ( Base ` ndx ) =/= ( le ` ndx )
6 3 5 setsnid 
 |-  ( Base ` O ) = ( Base ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
7 eqid 
 |-  ( le ` O ) = ( le ` O )
8 1 7 oduval 
 |-  D = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. )
9 8 fveq2i 
 |-  ( Base ` D ) = ( Base ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
10 6 2 9 3eqtr4i 
 |-  B = ( Base ` D )