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 40203
 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 40201 . 2 class TopLnd
2 vx . . . . . . . 8 setvar 𝑥
32cv 1537 . . . . . . 7 class 𝑥
43cuni 4801 . . . . . 6 class 𝑥
5 vy . . . . . . . 8 setvar 𝑦
65cv 1537 . . . . . . 7 class 𝑦
76cuni 4801 . . . . . 6 class 𝑦
84, 7wceq 1538 . . . . 5 wff 𝑥 = 𝑦
9 vz . . . . . . . . 9 setvar 𝑧
109cv 1537 . . . . . . . 8 class 𝑧
11 com 7563 . . . . . . . 8 class ω
12 cdom 8493 . . . . . . . 8 class
1310, 11, 12wbr 5031 . . . . . . 7 wff 𝑧 ≼ ω
1410cuni 4801 . . . . . . . 8 class 𝑧
154, 14wceq 1538 . . . . . . 7 wff 𝑥 = 𝑧
1613, 15wa 399 . . . . . 6 wff (𝑧 ≼ ω ∧ 𝑥 = 𝑧)
173cpw 4497 . . . . . 6 class 𝒫 𝑥
1816, 9, 17wrex 3107 . . . . 5 wff 𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧)
198, 18wi 4 . . . 4 wff ( 𝑥 = 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧))
2019, 5, 17wral 3106 . . 3 wff 𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧))
21 ctop 21508 . . 3 class Top
2220, 2, 21crab 3110 . 2 class {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧))}
231, 22wceq 1538 1 wff TopLnd = {𝑥 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑥( 𝑥 = 𝑦 → ∃𝑧 ∈ 𝒫 𝑥(𝑧 ≼ ω ∧ 𝑥 = 𝑧))}
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator