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

Definition df-ordt 15411
 Description: Define the order topology, given an order , written as below. A closed subbasis for the order topology is given by the closed rays and , along with itself. (Contributed by Mario Carneiro, 3-Sep-2015.)
Assertion
Ref Expression
df-ordt ordTop
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-ordt
StepHypRef Expression
1 cordt 15409 . 2 ordTop
2 vr . . 3
3 cvv 3047 . . 3
42cv 1445 . . . . . . . 8
54cdm 4837 . . . . . . 7
65csn 3970 . . . . . 6
7 vx . . . . . . . . 9
8 vy . . . . . . . . . . . . 13
98cv 1445 . . . . . . . . . . . 12
107cv 1445 . . . . . . . . . . . 12
119, 10, 4wbr 4405 . . . . . . . . . . 11
1211wn 3 . . . . . . . . . 10
1312, 8, 5crab 2743 . . . . . . . . 9
147, 5, 13cmpt 4464 . . . . . . . 8
1510, 9, 4wbr 4405 . . . . . . . . . . 11
1615wn 3 . . . . . . . . . 10
1716, 8, 5crab 2743 . . . . . . . . 9
187, 5, 17cmpt 4464 . . . . . . . 8
1914, 18cun 3404 . . . . . . 7
2019crn 4838 . . . . . 6
216, 20cun 3404 . . . . 5
22 cfi 7929 . . . . 5
2321, 22cfv 5585 . . . 4
24 ctg 15348 . . . 4
2523, 24cfv 5585 . . 3
262, 3, 25cmpt 4464 . 2
271, 26wceq 1446 1 ordTop
 Colors of variables: wff setvar class This definition is referenced by:  ordtval  20217
 Copyright terms: Public domain W3C validator