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

Definition df-ordt 16764
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 16762 . 2 class ordTop
2 vr . . 3 setvar 𝑟
3 cvv 3495 . . 3 class V
42cv 1527 . . . . . . . 8 class 𝑟
54cdm 5549 . . . . . . 7 class dom 𝑟
65csn 4559 . . . . . 6 class {dom 𝑟}
7 vx . . . . . . . . 9 setvar 𝑥
8 vy . . . . . . . . . . . . 13 setvar 𝑦
98cv 1527 . . . . . . . . . . . 12 class 𝑦
107cv 1527 . . . . . . . . . . . 12 class 𝑥
119, 10, 4wbr 5058 . . . . . . . . . . 11 wff 𝑦𝑟𝑥
1211wn 3 . . . . . . . . . 10 wff ¬ 𝑦𝑟𝑥
1312, 8, 5crab 3142 . . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}
147, 5, 13cmpt 5138 . . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥})
1510, 9, 4wbr 5058 . . . . . . . . . . 11 wff 𝑥𝑟𝑦
1615wn 3 . . . . . . . . . 10 wff ¬ 𝑥𝑟𝑦
1716, 8, 5crab 3142 . . . . . . . . 9 class {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}
187, 5, 17cmpt 5138 . . . . . . . 8 class (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})
1914, 18cun 3933 . . . . . . 7 class ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
2019crn 5550 . . . . . 6 class ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))
216, 20cun 3933 . . . . 5 class ({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))
22 cfi 8863 . . . . 5 class fi
2321, 22cfv 6349 . . . 4 class (fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))
24 ctg 16701 . . . 4 class topGen
2523, 24cfv 6349 . . 3 class (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦})))))
262, 3, 25cmpt 5138 . 2 class (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))
271, 26wceq 1528 1 wff ordTop = (𝑟 ∈ V ↦ (topGen‘(fi‘({dom 𝑟} ∪ ran ((𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑦𝑟𝑥}) ∪ (𝑥 ∈ dom 𝑟 ↦ {𝑦 ∈ dom 𝑟 ∣ ¬ 𝑥𝑟𝑦}))))))
Colors of variables: wff setvar class
This definition is referenced by:  ordtval  21727
  Copyright terms: Public domain W3C validator