Theorem otpsstr

Description: Functionality of a topological ordered space. (Contributed by Mario Carneiro, 12-Nov-2015) (Revised by AV, 9-Sep-2021)

	Ref	Expression
Hypothesis	otpsstr.w	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\right\}$$
Assertion	otpsstr	$$⊢K\mathrm{Struct}⟨1,10⟩$$

Proof

Step	Hyp	Ref	Expression
1		otpsstr.w	$$⊢K=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\right\}$$
2		1nn	$$⊢1\in \mathbb{N}$$
3		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
4		1lt9	$$⊢1<9$$
5		9nn	$$⊢9\in \mathbb{N}$$
6		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
7		9lt10	$$⊢9<10$$
8		10nn	$$⊢10\in \mathbb{N}$$
9		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
10	2 3 4 5 6 7 8 9	strle3	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩,⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩\right\}\mathrm{Struct}⟨1,10⟩$$
11	1 10	eqbrtri	$$⊢K\mathrm{Struct}⟨1,10⟩$$