# 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}=\mathrm{ODual}\left({O}\right)$
odubas.b ${⊢}{B}={\mathrm{Base}}_{{O}}$
Assertion odubas ${⊢}{B}={\mathrm{Base}}_{{D}}$

### Proof

Step Hyp Ref Expression
1 oduval.d ${⊢}{D}=\mathrm{ODual}\left({O}\right)$
2 odubas.b ${⊢}{B}={\mathrm{Base}}_{{O}}$
3 baseid ${⊢}\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$
4 1re ${⊢}1\in ℝ$
5 1lt10 ${⊢}1<10$
6 4 5 ltneii ${⊢}1\ne 10$
7 basendx ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}=1$
8 plendx ${⊢}{\le }_{\mathrm{ndx}}=10$
9 7 8 neeq12i ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}↔1\ne 10$
10 6 9 mpbir ${⊢}{\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$
11 3 10 setsnid ${⊢}{\mathrm{Base}}_{{O}}={\mathrm{Base}}_{\left({O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩\right)}$
12 eqid ${⊢}{\le }_{{O}}={\le }_{{O}}$
13 1 12 oduval ${⊢}{D}={O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩$
14 13 fveq2i ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{\left({O}\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_{{O}}}^{-1}⟩\right)}$
15 11 2 14 3eqtr4i ${⊢}{B}={\mathrm{Base}}_{{D}}$