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

Definition df-ordt 15984
 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 = (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))
Distinct variable group:   𝑥,𝑟,𝑦

Detailed syntax breakdown of Definition df-ordt
StepHypRef Expression
1 cordt 15982 . 2 class ordTop
2 vr . . 3 setvar 𝑟
3 cvv 3173 . . 3 class V
42cv 1474 . . . . . . . 8 class 𝑟
54cdm 5038 . . . . . . 7 class dom 𝑟
65csn 4125 . . . . . 6 class {dom 𝑟}
7 vx . . . . . . . . 9 setvar 𝑥
8 vy . . . . . . . . . . . . 13 setvar 𝑦
98cv 1474 . . . . . . . . . . . 12 class 𝑦
107cv 1474 . . . . . . . . . . . 12 class 𝑥
119, 10, 4wbr 4583 . . . . . . . . . . 11 wff 𝑦𝑟𝑥
1211wn 3 . . . . . . . . . 10 wff ¬ 𝑦𝑟𝑥
1312, 8, 5crab 2900 . . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}
147, 5, 13cmpt 4643 . . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥})
1510, 9, 4wbr 4583 . . . . . . . . . . 11 wff 𝑥𝑟𝑦
1615wn 3 . . . . . . . . . 10 wff ¬ 𝑥𝑟𝑦
1716, 8, 5crab 2900 . . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}
187, 5, 17cmpt 4643 . . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})
1914, 18cun 3538 . . . . . . 7 class ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
2019crn 5039 . . . . . 6 class ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
216, 20cun 3538 . . . . 5 class ({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))
22 cfi 8199 . . . . 5 class fi
2321, 22cfv 5804 . . . 4 class (fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))
24 ctg 15921 . . . 4 class topGen
2523, 24cfv 5804 . . 3 class (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))))
262, 3, 25cmpt 4643 . 2 class (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))
271, 26wceq 1475 1 wff ordTop = (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))
 Colors of variables: wff setvar class This definition is referenced by:  ordtval  20803
 Copyright terms: Public domain W3C validator