Description: The order 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 | otpsle | |- ( .<_ e. V -> .<_ = ( le ` K ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | otpsstr.w | |- K = { <. ( Base ` ndx ) , B >. , <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. } |
|
2 | 1 | otpsstr | |- K Struct <. 1 , ; 1 0 >. |
3 | pleid | |- le = Slot ( le ` ndx ) |
|
4 | snsstp3 | |- { <. ( le ` ndx ) , .<_ >. } C_ { <. ( Base ` ndx ) , B >. , <. ( TopSet ` ndx ) , J >. , <. ( le ` ndx ) , .<_ >. } |
|
5 | 4 1 | sseqtrri | |- { <. ( le ` ndx ) , .<_ >. } C_ K |
6 | 2 3 5 | strfv | |- ( .<_ e. V -> .<_ = ( le ` K ) ) |