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 21183
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 21181 . 2 class 2nd𝜔
2 vx . . . . . . 7 setvar 𝑥
32cv 1479 . . . . . 6 class 𝑥
4 com 7027 . . . . . 6 class ω
5 cdom 7913 . . . . . 6 class
63, 4, 5wbr 4623 . . . . 5 wff 𝑥 ≼ ω
7 ctg 16038 . . . . . . 7 class topGen
83, 7cfv 5857 . . . . . 6 class (topGen‘𝑥)
9 vj . . . . . . 7 setvar 𝑗
109cv 1479 . . . . . 6 class 𝑗
118, 10wceq 1480 . . . . 5 wff (topGen‘𝑥) = 𝑗
126, 11wa 384 . . . 4 wff (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)
13 ctb 20689 . . . 4 class TopBases
1412, 2, 13wrex 2909 . . 3 wff 𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)
1514, 9cab 2607 . 2 class {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
161, 15wceq 1480 1 wff 2nd𝜔 = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
Colors of variables: wff setvar class
This definition is referenced by:  is2ndc  21189
  Copyright terms: Public domain W3C validator