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

Definition df-topsep 40202
 Description: A topology is separable iff it has a countable dense subset. (Contributed by Stefan O'Rear, 8-Jan-2015.)
Assertion
Ref Expression
df-topsep TopSep = {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = 𝑗)}
Distinct variable group:   𝑥,𝑗

Detailed syntax breakdown of Definition df-topsep
StepHypRef Expression
1 ctopsep 40200 . 2 class TopSep
2 vx . . . . . . 7 setvar 𝑥
32cv 1537 . . . . . 6 class 𝑥
4 com 7563 . . . . . 6 class ω
5 cdom 8493 . . . . . 6 class
63, 4, 5wbr 5031 . . . . 5 wff 𝑥 ≼ ω
7 vj . . . . . . . . 9 setvar 𝑗
87cv 1537 . . . . . . . 8 class 𝑗
9 ccl 21633 . . . . . . . 8 class cls
108, 9cfv 6325 . . . . . . 7 class (cls‘𝑗)
113, 10cfv 6325 . . . . . 6 class ((cls‘𝑗)‘𝑥)
128cuni 4801 . . . . . 6 class 𝑗
1311, 12wceq 1538 . . . . 5 wff ((cls‘𝑗)‘𝑥) = 𝑗
146, 13wa 399 . . . 4 wff (𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = 𝑗)
1512cpw 4497 . . . 4 class 𝒫 𝑗
1614, 2, 15wrex 3107 . . 3 wff 𝑥 ∈ 𝒫 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = 𝑗)
17 ctop 21508 . . 3 class Top
1816, 7, 17crab 3110 . 2 class {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = 𝑗)}
191, 18wceq 1538 1 wff TopSep = {𝑗 ∈ Top ∣ ∃𝑥 ∈ 𝒫 𝑗(𝑥 ≼ ω ∧ ((cls‘𝑗)‘𝑥) = 𝑗)}
 Colors of variables: wff setvar class This definition is referenced by: (None)
 Copyright terms: Public domain W3C validator