MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ordt Unicode version

Definition df-ordt 13402
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.)
Assertion
Ref Expression
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 } ) ) ) ) ) )
Distinct variable group:    x, r, y

Detailed syntax breakdown of Definition df-ordt
StepHypRef Expression
1 cordt 13398 . 2  class ordTop
2 vr . . 3  set  r
3 cvv 2788 . . 3  class  _V
42cv 1622 . . . . . . . 8  class  r
54cdm 4689 . . . . . . 7  class  dom  r
65csn 3640 . . . . . 6  class  { dom  r }
7 vx . . . . . . . . 9  set  x
8 vy . . . . . . . . . . . . 13  set  y
98cv 1622 . . . . . . . . . . . 12  class  y
107cv 1622 . . . . . . . . . . . 12  class  x
119, 10, 4wbr 4023 . . . . . . . . . . 11  wff  y r x
1211wn 3 . . . . . . . . . 10  wff  -.  y
r x
1312, 8, 5crab 2547 . . . . . . . . 9  class  { y  e.  dom  r  |  -.  y r x }
147, 5, 13cmpt 4077 . . . . . . . 8  class  ( x  e.  dom  r  |->  { y  e.  dom  r  |  -.  y r x } )
1510, 9, 4wbr 4023 . . . . . . . . . . 11  wff  x r y
1615wn 3 . . . . . . . . . 10  wff  -.  x
r y
1716, 8, 5crab 2547 . . . . . . . . 9  class  { y  e.  dom  r  |  -.  x r y }
187, 5, 17cmpt 4077 . . . . . . . 8  class  ( x  e.  dom  r  |->  { y  e.  dom  r  |  -.  x r y } )
1914, 18cun 3150 . . . . . . 7  class  ( ( x  e.  dom  r  |->  { y  e.  dom  r  |  -.  y
r x } )  u.  ( x  e. 
dom  r  |->  { y  e.  dom  r  |  -.  x r y } ) )
2019crn 4690 . . . . . 6  class  ran  (
( x  e.  dom  r  |->  { y  e. 
dom  r  |  -.  y r x }
)  u.  ( x  e.  dom  r  |->  { y  e.  dom  r  |  -.  x r y } ) )
216, 20cun 3150 . . . . 5  class  ( { 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 } ) ) )
22 cfi 7164 . . . . 5  class  fi
2321, 22cfv 5255 . . . 4  class  ( 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 ctg 13342 . . . 4  class  topGen
2523, 24cfv 5255 . . 3  class  ( 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 } ) ) ) ) )
262, 3, 25cmpt 4077 . 2  class  ( 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 } ) ) ) ) ) )
271, 26wceq 1623 1  wff 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 } ) ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  ordtval  16919
  Copyright terms: Public domain W3C validator