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 ⊢ 𝐷 = ( ODual ‘ 𝑂 )
odubas.b ⊢ 𝐵 = ( Base ‘ 𝑂 )
Assertion odubas 𝐵 = ( Base ‘ 𝐷 )

Proof

Step Hyp Ref Expression
1 oduval.d ⊢ 𝐷 = ( ODual ‘ 𝑂 )
2 odubas.b ⊢ 𝐵 = ( Base ‘ 𝑂 )
3 baseid ⊢ Base = Slot ( Base ‘ ndx )
4 plendxnbasendx ⊢ ( le ‘ ndx ) ≠ ( Base ‘ ndx )
5 4 necomi ⊢ ( Base ‘ ndx ) ≠ ( le ‘ ndx )
6 3 5 setsnid ⊢ ( Base ‘ 𝑂 ) = ( Base ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) )
7 eqid ⊢ ( le ‘ 𝑂 ) = ( le ‘ 𝑂 )
8 1 7 oduval ⊢ 𝐷 = ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ )
9 8 fveq2i ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ ( 𝑂 sSet ⟨ ( le ‘ ndx ) , ◡ ( le ‘ 𝑂 ) ⟩ ) )
10 6 2 9 3eqtr4i ⊢ 𝐵 = ( Base ‘ 𝐷 )