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=\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		plendxnbasendx	$$⊢{\le }_{\mathrm{ndx}}\ne {\mathrm{Base}}_{\mathrm{ndx}}$$
5	4	necomi	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {\le }_{\mathrm{ndx}}$$
6	3 5	setsnid	$$⊢{\mathrm{Base}}_O={\mathrm{Base}}_{\left(O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_O}^{-1}⟩\right)}$$
7		eqid	$$⊢{\le }_O={\le }_O$$
8	1 7	oduval	$$⊢D=O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_O}^{-1}⟩$$
9	8	fveq2i	$$⊢{\mathrm{Base}}_D={\mathrm{Base}}_{\left(O\mathrm{sSet}⟨{\le }_{\mathrm{ndx}},{{\le }_O}^{-1}⟩\right)}$$
10	6 2 9	3eqtr4i	$$⊢B={\mathrm{Base}}_D$$