Theorem ipostr

Description: The structure of df-ipo is a structure defining indices up to 11. (Contributed by Mario Carneiro, 25-Oct-2015)

	Ref	Expression
Assertion	ipostr	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\underset{\dot{}}{\perp }⟩\right\}\right)\mathrm{Struct}⟨1,11⟩$$

Proof

Step	Hyp	Ref	Expression
1		1nn	$$⊢1\in \mathbb{N}$$
2		basendx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}=1$$
3		1lt9	$$⊢1<9$$
4		9nn	$$⊢9\in \mathbb{N}$$
5		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
6	1 2 3 4 5	strle2	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\mathrm{Struct}⟨1,9⟩$$
7		10nn	$$⊢10\in \mathbb{N}$$
8		plendx	$$⊢{\le }_{\mathrm{ndx}}=10$$
9		1nn0	$$⊢1\in {\mathbb{N}}_0$$
10		0nn0	$$⊢0\in {\mathbb{N}}_0$$
11		0lt1	$$⊢0<1$$
12	9 10 1 11	declt	$$⊢10<11$$
13	9 1	decnncl	$$⊢11\in \mathbb{N}$$
14		ocndx	$$⊢\mathrm{oc}\left(\mathrm{ndx}\right)=11$$
15	7 8 12 13 14	strle2	$$⊢\left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\underset{\dot{}}{\perp }⟩\right\}\mathrm{Struct}⟨10,11⟩$$
16		9lt10	$$⊢9<10$$
17	6 15 16	strleun	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),J⟩\right\}\cup \left\{⟨{\le }_{\mathrm{ndx}},\underset{\dot{}}{\le }⟩,⟨\mathrm{oc}\left(\mathrm{ndx}\right),\underset{\dot{}}{\perp }⟩\right\}\right)\mathrm{Struct}⟨1,11⟩$$