MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-1stc Structured version   Visualization version   GIF version

Definition df-1stc 22571
Description: Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.)
Assertion
Ref Expression
df-1stc 1stω = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))}
Distinct variable group:   𝑥,𝑗,𝑦,𝑧

Detailed syntax breakdown of Definition df-1stc
StepHypRef Expression
1 c1stc 22569 . 2 class 1stω
2 vy . . . . . . . 8 setvar 𝑦
32cv 1540 . . . . . . 7 class 𝑦
4 com 7700 . . . . . . 7 class ω
5 cdom 8705 . . . . . . 7 class
63, 4, 5wbr 5078 . . . . . 6 wff 𝑦 ≼ ω
7 vx . . . . . . . . 9 setvar 𝑥
8 vz . . . . . . . . 9 setvar 𝑧
97, 8wel 2110 . . . . . . . 8 wff 𝑥𝑧
107cv 1540 . . . . . . . . 9 class 𝑥
118cv 1540 . . . . . . . . . . . 12 class 𝑧
1211cpw 4538 . . . . . . . . . . 11 class 𝒫 𝑧
133, 12cin 3890 . . . . . . . . . 10 class (𝑦 ∩ 𝒫 𝑧)
1413cuni 4844 . . . . . . . . 9 class (𝑦 ∩ 𝒫 𝑧)
1510, 14wcel 2109 . . . . . . . 8 wff 𝑥 (𝑦 ∩ 𝒫 𝑧)
169, 15wi 4 . . . . . . 7 wff (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧))
17 vj . . . . . . . 8 setvar 𝑗
1817cv 1540 . . . . . . 7 class 𝑗
1916, 8, 18wral 3065 . . . . . 6 wff 𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧))
206, 19wa 395 . . . . 5 wff (𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
2118cpw 4538 . . . . 5 class 𝒫 𝑗
2220, 2, 21wrex 3066 . . . 4 wff 𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
2318cuni 4844 . . . 4 class 𝑗
2422, 7, 23wral 3065 . . 3 wff 𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
25 ctop 22023 . . 3 class Top
2624, 17, 25crab 3069 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))}
271, 26wceq 1541 1 wff 1stω = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))}
Colors of variables: wff setvar class
This definition is referenced by:  is1stc  22573
  Copyright terms: Public domain W3C validator