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 ‘ 𝐷 )