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 41586
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 41584 . 2 class TopLnd
2 vx . . . . . . . 8 setvar π‘₯
32cv 1541 . . . . . . 7 class π‘₯
43cuni 4866 . . . . . 6 class βˆͺ π‘₯
5 vy . . . . . . . 8 setvar 𝑦
65cv 1541 . . . . . . 7 class 𝑦
76cuni 4866 . . . . . 6 class βˆͺ 𝑦
84, 7wceq 1542 . . . . 5 wff βˆͺ π‘₯ = βˆͺ 𝑦
9 vz . . . . . . . . 9 setvar 𝑧
109cv 1541 . . . . . . . 8 class 𝑧
11 com 7803 . . . . . . . 8 class Ο‰
12 cdom 8884 . . . . . . . 8 class β‰Ό
1310, 11, 12wbr 5106 . . . . . . 7 wff 𝑧 β‰Ό Ο‰
1410cuni 4866 . . . . . . . 8 class βˆͺ 𝑧
154, 14wceq 1542 . . . . . . 7 wff βˆͺ π‘₯ = βˆͺ 𝑧
1613, 15wa 397 . . . . . 6 wff (𝑧 β‰Ό Ο‰ ∧ βˆͺ π‘₯ = βˆͺ 𝑧)
173cpw 4561 . . . . . 6 class 𝒫 π‘₯
1816, 9, 17wrex 3070 . . . . 5 wff βˆƒπ‘§ ∈ 𝒫 π‘₯(𝑧 β‰Ό Ο‰ ∧ βˆͺ π‘₯ = βˆͺ 𝑧)
198, 18wi 4 . . . 4 wff (βˆͺ π‘₯ = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ 𝒫 π‘₯(𝑧 β‰Ό Ο‰ ∧ βˆͺ π‘₯ = βˆͺ 𝑧))
2019, 5, 17wral 3061 . . 3 wff βˆ€π‘¦ ∈ 𝒫 π‘₯(βˆͺ π‘₯ = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ 𝒫 π‘₯(𝑧 β‰Ό Ο‰ ∧ βˆͺ π‘₯ = βˆͺ 𝑧))
21 ctop 22258 . . 3 class Top
2220, 2, 21crab 3406 . 2 class {π‘₯ ∈ Top ∣ βˆ€π‘¦ ∈ 𝒫 π‘₯(βˆͺ π‘₯ = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ 𝒫 π‘₯(𝑧 β‰Ό Ο‰ ∧ βˆͺ π‘₯ = βˆͺ 𝑧))}
231, 22wceq 1542 1 wff TopLnd = {π‘₯ ∈ Top ∣ βˆ€π‘¦ ∈ 𝒫 π‘₯(βˆͺ π‘₯ = βˆͺ 𝑦 β†’ βˆƒπ‘§ ∈ 𝒫 π‘₯(𝑧 β‰Ό Ο‰ ∧ βˆͺ π‘₯ = βˆͺ 𝑧))}
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator