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

Definition df-1stc 22048
 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 22046 . 2 class 1stω
2 vy . . . . . . . 8 setvar 𝑦
32cv 1537 . . . . . . 7 class 𝑦
4 com 7564 . . . . . . 7 class ω
5 cdom 8494 . . . . . . 7 class
63, 4, 5wbr 5033 . . . . . 6 wff 𝑦 ≼ ω
7 vx . . . . . . . . 9 setvar 𝑥
8 vz . . . . . . . . 9 setvar 𝑧
97, 8wel 2113 . . . . . . . 8 wff 𝑥𝑧
107cv 1537 . . . . . . . . 9 class 𝑥
118cv 1537 . . . . . . . . . . . 12 class 𝑧
1211cpw 4500 . . . . . . . . . . 11 class 𝒫 𝑧
133, 12cin 3883 . . . . . . . . . 10 class (𝑦 ∩ 𝒫 𝑧)
1413cuni 4803 . . . . . . . . 9 class (𝑦 ∩ 𝒫 𝑧)
1510, 14wcel 2112 . . . . . . . 8 wff 𝑥 (𝑦 ∩ 𝒫 𝑧)
169, 15wi 4 . . . . . . 7 wff (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧))
17 vj . . . . . . . 8 setvar 𝑗
1817cv 1537 . . . . . . 7 class 𝑗
1916, 8, 18wral 3109 . . . . . 6 wff 𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧))
206, 19wa 399 . . . . 5 wff (𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
2118cpw 4500 . . . . 5 class 𝒫 𝑗
2220, 2, 21wrex 3110 . . . 4 wff 𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
2318cuni 4803 . . . 4 class 𝑗
2422, 7, 23wral 3109 . . 3 wff 𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
25 ctop 21502 . . 3 class Top
2624, 17, 25crab 3113 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))}
271, 26wceq 1538 1 wff 1stω = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))}
 Colors of variables: wff setvar class This definition is referenced by:  is1stc  22050
 Copyright terms: Public domain W3C validator