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 21147
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 21145 . 2 class 1st𝜔
2 vy . . . . . . . 8 setvar 𝑦
32cv 1479 . . . . . . 7 class 𝑦
4 com 7013 . . . . . . 7 class ω
5 cdom 7898 . . . . . . 7 class
63, 4, 5wbr 4618 . . . . . 6 wff 𝑦 ≼ ω
7 vx . . . . . . . . 9 setvar 𝑥
8 vz . . . . . . . . 9 setvar 𝑧
97, 8wel 1993 . . . . . . . 8 wff 𝑥𝑧
107cv 1479 . . . . . . . . 9 class 𝑥
118cv 1479 . . . . . . . . . . . 12 class 𝑧
1211cpw 4135 . . . . . . . . . . 11 class 𝒫 𝑧
133, 12cin 3559 . . . . . . . . . 10 class (𝑦 ∩ 𝒫 𝑧)
1413cuni 4407 . . . . . . . . 9 class (𝑦 ∩ 𝒫 𝑧)
1510, 14wcel 1992 . . . . . . . 8 wff 𝑥 (𝑦 ∩ 𝒫 𝑧)
169, 15wi 4 . . . . . . 7 wff (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧))
17 vj . . . . . . . 8 setvar 𝑗
1817cv 1479 . . . . . . 7 class 𝑗
1916, 8, 18wral 2912 . . . . . 6 wff 𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧))
206, 19wa 384 . . . . 5 wff (𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
2118cpw 4135 . . . . 5 class 𝒫 𝑗
2220, 2, 21wrex 2913 . . . 4 wff 𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
2318cuni 4407 . . . 4 class 𝑗
2422, 7, 23wral 2912 . . 3 wff 𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))
25 ctop 20612 . . 3 class Top
2624, 17, 25crab 2916 . 2 class {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))}
271, 26wceq 1480 1 wff 1st𝜔 = {𝑗 ∈ Top ∣ ∀𝑥 𝑗𝑦 ∈ 𝒫 𝑗(𝑦 ≼ ω ∧ ∀𝑧𝑗 (𝑥𝑧𝑥 (𝑦 ∩ 𝒫 𝑧)))}
Colors of variables: wff setvar class
This definition is referenced by:  is1stc  21149
  Copyright terms: Public domain W3C validator