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	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ⊥ ⟩ } ) Struct ⟨ 1 , ; 1 1 ⟩

Proof

Step	Hyp	Ref	Expression
1		1nn	⊢ 1 ∈ ℕ
2		basendx	⊢ ( Base ‘ ndx ) = 1
3		1lt9	⊢ 1 < 9
4		9nn	⊢ 9 ∈ ℕ
5		tsetndx	⊢ ( TopSet ‘ ndx ) = 9
6	1 2 3 4 5	strle2	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } Struct ⟨ 1 , 9 ⟩
7		10nn	⊢ ; 1 0 ∈ ℕ
8		plendx	⊢ ( le ‘ ndx ) = ; 1 0
9		1nn0	⊢ 1 ∈ ℕ0
10		0nn0	⊢ 0 ∈ ℕ0
11		0lt1	⊢ 0 < 1
12	9 10 1 11	declt	⊢ ; 1 0 < ; 1 1
13	9 1	decnncl	⊢ ; 1 1 ∈ ℕ
14		ocndx	⊢ ( oc ‘ ndx ) = ; 1 1
15	7 8 12 13 14	strle2	⊢ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ⊥ ⟩ } Struct ⟨ ; 1 0 , ; 1 1 ⟩
16		9lt10	⊢ 9 < ; 1 0
17	6 15 16	strleun	⊢ ( { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ } ∪ { ⟨ ( le ‘ ndx ) , ≤ ⟩ , ⟨ ( oc ‘ ndx ) , ⊥ ⟩ } ) Struct ⟨ 1 , ; 1 1 ⟩