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	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ }
Assertion	otpsstr	⊢ 𝐾 Struct ⟨ 1 , ; 1 0 ⟩

Proof

Step	Hyp	Ref	Expression
1		otpsstr.w	⊢ 𝐾 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ }
2		1nn	⊢ 1 ∈ ℕ
3		basendx	⊢ ( Base ‘ ndx ) = 1
4		1lt9	⊢ 1 < 9
5		9nn	⊢ 9 ∈ ℕ
6		tsetndx	⊢ ( TopSet ‘ ndx ) = 9
7		9lt10	⊢ 9 < ; 1 0
8		10nn	⊢ ; 1 0 ∈ ℕ
9		plendx	⊢ ( le ‘ ndx ) = ; 1 0
10	2 3 4 5 6 7 8 9	strle3	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( TopSet ‘ ndx ) , 𝐽 ⟩ , ⟨ ( le ‘ ndx ) , ≤ ⟩ } Struct ⟨ 1 , ; 1 0 ⟩
11	1 10	eqbrtri	⊢ 𝐾 Struct ⟨ 1 , ; 1 0 ⟩