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

Definition df-2ndc 22589
Description: Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.)
Assertion
Ref Expression
df-2ndc 2ndω = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
Distinct variable group:   𝑥,𝑗

Detailed syntax breakdown of Definition df-2ndc
StepHypRef Expression
1 c2ndc 22587 . 2 class 2ndω
2 vx . . . . . . 7 setvar 𝑥
32cv 1541 . . . . . 6 class 𝑥
4 com 7706 . . . . . 6 class ω
5 cdom 8714 . . . . . 6 class
63, 4, 5wbr 5079 . . . . 5 wff 𝑥 ≼ ω
7 ctg 17146 . . . . . . 7 class topGen
83, 7cfv 6432 . . . . . 6 class (topGen‘𝑥)
9 vj . . . . . . 7 setvar 𝑗
109cv 1541 . . . . . 6 class 𝑗
118, 10wceq 1542 . . . . 5 wff (topGen‘𝑥) = 𝑗
126, 11wa 396 . . . 4 wff (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)
13 ctb 22093 . . . 4 class TopBases
1412, 2, 13wrex 3067 . . 3 wff 𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)
1514, 9cab 2717 . 2 class {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
161, 15wceq 1542 1 wff 2ndω = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
Colors of variables: wff setvar class
This definition is referenced by:  is2ndc  22595
  Copyright terms: Public domain W3C validator