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

Definition df-1stc 21290
 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 21288 . 2 class 1st𝜔
2 vy . . . . . . . 8 setvar 𝑦
32cv 1522 . . . . . . 7 class 𝑦
4 com 7107 . . . . . . 7 class ω
5 cdom 7995 . . . . . . 7 class
63, 4, 5wbr 4685 . . . . . 6 wff 𝑦 ≼ ω
7 vx . . . . . . . . 9 setvar 𝑥
8 vz . . . . . . . . 9 setvar 𝑧
97, 8wel 2031 . . . . . . . 8 wff 𝑥𝑧
107cv 1522 . . . . . . . . 9 class 𝑥
118cv 1522 . . . . . . . . . . . 12 class 𝑧
1211cpw 4191 . . . . . . . . . . 11 class 𝒫 𝑧
133, 12cin 3606 . . . . . . . . . 10 class (𝑦 ∩ 𝒫 𝑧)
1413cuni 4468 . . . . . . . . 9 class (𝑦 ∩ 𝒫 𝑧)
1510, 14wcel 2030 . . . . . . . 8 wff 𝑥 (𝑦 ∩ 𝒫 𝑧)
169, 15wi 4 . . . . . . 7 wff (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧))
17 vj . . . . . . . 8 setvar 𝑗
1817cv 1522 . . . . . . 7 class 𝑗
1916, 8, 18wral 2941 . . . . . 6 wff 𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧))
206, 19wa 383 . . . . 5 wff (𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
2118cpw 4191 . . . . 5 class 𝒫 𝑗
2220, 2, 21wrex 2942 . . . 4 wff 𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
2318cuni 4468 . . . 4 class 𝑗
2422, 7, 23wral 2941 . . 3 wff 𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
25 ctop 20746 . . 3 class Top
2624, 17, 25crab 2945 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))}
271, 26wceq 1523 1 wff 1st𝜔 = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))}
 Colors of variables: wff setvar class This definition is referenced by:  is1stc  21292
 Copyright terms: Public domain W3C validator