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

Definition df-ordt 13717
 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 13713 . 2 ordTop
2 vr . . 3
3 cvv 2948 . . 3
42cv 1651 . . . . . . . 8
54cdm 4870 . . . . . . 7
65csn 3806 . . . . . 6
7 vx . . . . . . . . 9
8 vy . . . . . . . . . . . . 13
98cv 1651 . . . . . . . . . . . 12
107cv 1651 . . . . . . . . . . . 12
119, 10, 4wbr 4204 . . . . . . . . . . 11
1211wn 3 . . . . . . . . . 10
1312, 8, 5crab 2701 . . . . . . . . 9
147, 5, 13cmpt 4258 . . . . . . . 8
1510, 9, 4wbr 4204 . . . . . . . . . . 11
1615wn 3 . . . . . . . . . 10
1716, 8, 5crab 2701 . . . . . . . . 9
187, 5, 17cmpt 4258 . . . . . . . 8
1914, 18cun 3310 . . . . . . 7
2019crn 4871 . . . . . 6
216, 20cun 3310 . . . . 5
22 cfi 7407 . . . . 5
2321, 22cfv 5446 . . . 4
24 ctg 13657 . . . 4
2523, 24cfv 5446 . . 3
262, 3, 25cmpt 4258 . 2
271, 26wceq 1652 1 ordTop
 Colors of variables: wff set class This definition is referenced by:  ordtval  17245
 Copyright terms: Public domain W3C validator