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 ⊢ ≤ ndx ≠ Base ndx
5 4 necomi ⊢ Base ndx ≠ ≤ ndx
6 3 5 setsnid ⊢ Base O = Base O sSet ≤ ndx ≤ O -1
7 eqid ⊢ ≤ O = ≤ O
8 1 7 oduval ⊢ D = O sSet ≤ ndx ≤ O -1
9 8 fveq2i ⊢ Base D = Base O sSet ≤ ndx ≤ O -1
10 6 2 9 3eqtr4i ⊢ B = Base D