Metamath Proof Explorer

Definition df-ordt

Description: Define the order topology, given an order <_ , written as r below. A closed subbasis for the order topology is given by the closed rays [ y , +oo ) = { z e. X | y <_ z } and ( -oo , y ] = { z e. X | z <_ y } , along with ( -oo , +oo ) = X itself. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion df-ordt ⊢ordTop=r∈V⟼topGen⁡fi⁡dom⁡r∪ran⁡x∈dom⁡r⟼y∈dom⁡r|¬yrx∪x∈dom⁡r⟼y∈dom⁡r|¬xry

Detailed syntax breakdown

Step Hyp Ref Expression
0 cordt classordTop
1 vr setvarr
2 cvv classV
3 ctg classtopGen
4 cfi classfi
5 1 cv setvarr
6 5 cdm classdom⁡r
7 6 csn classdom⁡r
8 vx setvarx
9 vy setvary
10 9 cv setvary
11 8 cv setvarx
12 10 11 5 wbr wffyrx
13 12 wn wff¬yrx
14 13 9 6 crab classy∈dom⁡r|¬yrx
15 8 6 14 cmpt classx∈dom⁡r⟼y∈dom⁡r|¬yrx
16 11 10 5 wbr wffxry
17 16 wn wff¬xry
18 17 9 6 crab classy∈dom⁡r|¬xry
19 8 6 18 cmpt classx∈dom⁡r⟼y∈dom⁡r|¬xry
20 15 19 cun classx∈dom⁡r⟼y∈dom⁡r|¬yrx∪x∈dom⁡r⟼y∈dom⁡r|¬xry
21 20 crn classran⁡x∈dom⁡r⟼y∈dom⁡r|¬yrx∪x∈dom⁡r⟼y∈dom⁡r|¬xry
22 7 21 cun classdom⁡r∪ran⁡x∈dom⁡r⟼y∈dom⁡r|¬yrx∪x∈dom⁡r⟼y∈dom⁡r|¬xry
23 22 4 cfv classfi⁡dom⁡r∪ran⁡x∈dom⁡r⟼y∈dom⁡r|¬yrx∪x∈dom⁡r⟼y∈dom⁡r|¬xry
24 23 3 cfv classtopGen⁡fi⁡dom⁡r∪ran⁡x∈dom⁡r⟼y∈dom⁡r|¬yrx∪x∈dom⁡r⟼y∈dom⁡r|¬xry
25 1 2 24 cmpt classr∈V⟼topGen⁡fi⁡dom⁡r∪ran⁡x∈dom⁡r⟼y∈dom⁡r|¬yrx∪x∈dom⁡r⟼y∈dom⁡r|¬xry
26 0 25 wceq wffordTop=r∈V⟼topGen⁡fi⁡dom⁡r∪ran⁡x∈dom⁡r⟼y∈dom⁡r|¬yrx∪x∈dom⁡r⟼y∈dom⁡r|¬xry