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 e. _V |-> ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cordt 
 |-  ordTop
1 vr 
 |-  r
2 cvv 
 |-  _V
3 ctg 
 |-  topGen
4 cfi 
 |-  fi
5 1 cv 
 |-  r
6 5 cdm 
 |-  dom r
7 6 csn 
 |-  { dom r }
8 vx 
 |-  x
9 vy 
 |-  y
10 9 cv 
 |-  y
11 8 cv 
 |-  x
12 10 11 5 wbr 
 |-  y r x
13 12 wn 
 |-  -. y r x
14 13 9 6 crab 
 |-  { y e. dom r | -. y r x }
15 8 6 14 cmpt 
 |-  ( x e. dom r |-> { y e. dom r | -. y r x } )
16 11 10 5 wbr 
 |-  x r y
17 16 wn 
 |-  -. x r y
18 17 9 6 crab 
 |-  { y e. dom r | -. x r y }
19 8 6 18 cmpt 
 |-  ( x e. dom r |-> { y e. dom r | -. x r y } )
20 15 19 cun 
 |-  ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) )
21 20 crn 
 |-  ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) )
22 7 21 cun 
 |-  ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) )
23 22 4 cfv 
 |-  ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) )
24 23 3 cfv 
 |-  ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) )
25 1 2 24 cmpt 
 |-  ( r e. _V |-> ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) ) )
26 0 25 wceq 
 |-  ordTop = ( r e. _V |-> ( topGen ` ( fi ` ( { dom r } u. ran ( ( x e. dom r |-> { y e. dom r | -. y r x } ) u. ( x e. dom r |-> { y e. dom r | -. x r y } ) ) ) ) ) )