Metamath Proof Explorer

Theorem odubas

Description: Base set of an order dual structure. (Contributed by Stefan O'Rear, 29-Jan-2015)

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 1re 
 |-  1 e. RR
5 1lt10 
 |-  1 < ; 1 0
6 4 5 ltneii 
 |-  1 =/= ; 1 0
7 basendx 
 |-  ( Base ` ndx ) = 1
8 plendx 
 |-  ( le ` ndx ) = ; 1 0
9 7 8 neeq12i 
 |-  ( ( Base ` ndx ) =/= ( le ` ndx ) <-> 1 =/= ; 1 0 )
10 6 9 mpbir 
 |-  ( Base ` ndx ) =/= ( le ` ndx )
11 3 10 setsnid 
 |-  ( Base ` O ) = ( Base ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
12 eqid 
 |-  ( le ` O ) = ( le ` O )
13 1 12 oduval 
 |-  D = ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. )
14 13 fveq2i 
 |-  ( Base ` D ) = ( Base ` ( O sSet <. ( le ` ndx ) , `' ( le ` O ) >. ) )
15 11 2 14 3eqtr4i 
 |-  B = ( Base ` D )