This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⟩