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}}\leftrightarrow 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$$