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 17446
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 17444 . 2 class ordTop
2 vr . . 3 setvar π‘Ÿ
3 cvv 3474 . . 3 class V
42cv 1540 . . . . . . . 8 class π‘Ÿ
54cdm 5676 . . . . . . 7 class dom π‘Ÿ
65csn 4628 . . . . . 6 class {dom π‘Ÿ}
7 vx . . . . . . . . 9 setvar π‘₯
8 vy . . . . . . . . . . . . 13 setvar 𝑦
98cv 1540 . . . . . . . . . . . 12 class 𝑦
107cv 1540 . . . . . . . . . . . 12 class π‘₯
119, 10, 4wbr 5148 . . . . . . . . . . 11 wff π‘¦π‘Ÿπ‘₯
1211wn 3 . . . . . . . . . 10 wff Β¬ π‘¦π‘Ÿπ‘₯
1312, 8, 5crab 3432 . . . . . . . . 9 class {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘¦π‘Ÿπ‘₯}
147, 5, 13cmpt 5231 . . . . . . . 8 class (π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘¦π‘Ÿπ‘₯})
1510, 9, 4wbr 5148 . . . . . . . . . . 11 wff π‘₯π‘Ÿπ‘¦
1615wn 3 . . . . . . . . . 10 wff Β¬ π‘₯π‘Ÿπ‘¦
1716, 8, 5crab 3432 . . . . . . . . 9 class {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘₯π‘Ÿπ‘¦}
187, 5, 17cmpt 5231 . . . . . . . 8 class (π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘₯π‘Ÿπ‘¦})
1914, 18cun 3946 . . . . . . 7 class ((π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘¦π‘Ÿπ‘₯}) βˆͺ (π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘₯π‘Ÿπ‘¦}))
2019crn 5677 . . . . . 6 class ran ((π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘¦π‘Ÿπ‘₯}) βˆͺ (π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘₯π‘Ÿπ‘¦}))
216, 20cun 3946 . . . . 5 class ({dom π‘Ÿ} βˆͺ ran ((π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘¦π‘Ÿπ‘₯}) βˆͺ (π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘₯π‘Ÿπ‘¦})))
22 cfi 9404 . . . . 5 class fi
2321, 22cfv 6543 . . . 4 class (fiβ€˜({dom π‘Ÿ} βˆͺ ran ((π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘¦π‘Ÿπ‘₯}) βˆͺ (π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘₯π‘Ÿπ‘¦}))))
24 ctg 17382 . . . 4 class topGen
2523, 24cfv 6543 . . 3 class (topGenβ€˜(fiβ€˜({dom π‘Ÿ} βˆͺ ran ((π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘¦π‘Ÿπ‘₯}) βˆͺ (π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘₯π‘Ÿπ‘¦})))))
262, 3, 25cmpt 5231 . 2 class (π‘Ÿ ∈ V ↦ (topGenβ€˜(fiβ€˜({dom π‘Ÿ} βˆͺ ran ((π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘¦π‘Ÿπ‘₯}) βˆͺ (π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘₯π‘Ÿπ‘¦}))))))
271, 26wceq 1541 1 wff ordTop = (π‘Ÿ ∈ V ↦ (topGenβ€˜(fiβ€˜({dom π‘Ÿ} βˆͺ ran ((π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘¦π‘Ÿπ‘₯}) βˆͺ (π‘₯ ∈ dom π‘Ÿ ↦ {𝑦 ∈ dom π‘Ÿ ∣ Β¬ π‘₯π‘Ÿπ‘¦}))))))
Colors of variables: wff setvar class
This definition is referenced by:  ordtval  22692
  Copyright terms: Public domain W3C validator