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 = { <. ( Base ` ndx ) , B >. , <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }
Assertion	otpsstr	|- K Struct <. 1 , ; 1 0 >.

Proof

Step	Hyp	Ref	Expression
1		otpsstr.w	|- K = { <. ( Base ` ndx ) , B >. , <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. }
2		1nn	|- 1 e. NN
3		basendx	|- ( Base ` ndx ) = 1
4		1lt9	|- 1 < 9
5		9nn	|- 9 e. NN
6		tsetndx	|- ( TopSet ` ndx ) = 9
7		9lt10	|- 9 < ; 1 0
8		10nn	|- ; 1 0 e. NN
9		plendx	|- ( le ` ndx ) = ; 1 0
10	2 3 4 5 6 7 8 9	strle3	|- { <. ( Base ` ndx ) , B >. , <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. } Struct <. 1 , ; 1 0 >.
11	1 10	eqbrtri	|- K Struct <. 1 , ; 1 0 >.