Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-toplnd Structured version   Visualization version   GIF version

Definition df-toplnd 40744
Description: A topology is Lindelöf iff every open cover has a countable subcover. (Contributed by Stefan O'Rear, 8-Jan-2015.)
Assertion
Ref Expression
df-toplnd TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧))}
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-toplnd
StepHypRef Expression
1 ctoplnd 40742 . 2 class TopLnd
2 vx . . . . . . . 8 setvar 𝑥
32cv 1542 . . . . . . 7 class 𝑥
43cuni 4819 . . . . . 6 class 𝑥
5 vy . . . . . . . 8 setvar 𝑦
65cv 1542 . . . . . . 7 class 𝑦
76cuni 4819 . . . . . 6 class 𝑦
84, 7wceq 1543 . . . . 5 wff 𝑥 = 𝑦
9 vz . . . . . . . . 9 setvar 𝑧
109cv 1542 . . . . . . . 8 class 𝑧
11 com 7644 . . . . . . . 8 class ω
12 cdom 8624 . . . . . . . 8 class
1310, 11, 12wbr 5053 . . . . . . 7 wff 𝑧 ≼ ω
1410cuni 4819 . . . . . . . 8 class 𝑧
154, 14wceq 1543 . . . . . . 7 wff 𝑥 = 𝑧
1613, 15wa 399 . . . . . 6 wff (𝑧 ≼ ω ∧ 𝑥 = 𝑧)
173cpw 4513 . . . . . 6 class 𝒫 𝑥
1816, 9, 17wrex 3062 . . . . 5 wff 𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧)
198, 18wi 4 . . . 4 wff ( 𝑥 = 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧))
2019, 5, 17wral 3061 . . 3 wff 𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧))
21 ctop 21790 . . 3 class Top
2220, 2, 21crab 3065 . 2 class {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧))}
231, 22wceq 1543 1 wff TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧))}
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator