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 22814
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 22812 . 2 class 2ndΟ‰
2 vx . . . . . . 7 setvar π‘₯
32cv 1541 . . . . . 6 class π‘₯
4 com 7806 . . . . . 6 class Ο‰
5 cdom 8887 . . . . . 6 class β‰Ό
63, 4, 5wbr 5109 . . . . 5 wff π‘₯ β‰Ό Ο‰
7 ctg 17327 . . . . . . 7 class topGen
83, 7cfv 6500 . . . . . 6 class (topGenβ€˜π‘₯)
9 vj . . . . . . 7 setvar 𝑗
109cv 1541 . . . . . 6 class 𝑗
118, 10wceq 1542 . . . . 5 wff (topGenβ€˜π‘₯) = 𝑗
126, 11wa 397 . . . 4 wff (π‘₯ β‰Ό Ο‰ ∧ (topGenβ€˜π‘₯) = 𝑗)
13 ctb 22318 . . . 4 class TopBases
1412, 2, 13wrex 3070 . . 3 wff βˆƒπ‘₯ ∈ TopBases (π‘₯ β‰Ό Ο‰ ∧ (topGenβ€˜π‘₯) = 𝑗)
1514, 9cab 2710 . 2 class {𝑗 ∣ βˆƒπ‘₯ ∈ TopBases (π‘₯ β‰Ό Ο‰ ∧ (topGenβ€˜π‘₯) = 𝑗)}
161, 15wceq 1542 1 wff 2ndΟ‰ = {𝑗 ∣ βˆƒπ‘₯ ∈ TopBases (π‘₯ β‰Ό Ο‰ ∧ (topGenβ€˜π‘₯) = 𝑗)}
Colors of variables: wff setvar class
This definition is referenced by:  is2ndc  22820
  Copyright terms: Public domain W3C validator