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 22048
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 22046 . 2 class 2ndω
2 vx . . . . . . 7 setvar 𝑥
32cv 1537 . . . . . 6 class 𝑥
4 com 7564 . . . . . 6 class ω
5 cdom 8494 . . . . . 6 class
63, 4, 5wbr 5033 . . . . 5 wff 𝑥 ≼ ω
7 ctg 16706 . . . . . . 7 class topGen
83, 7cfv 6328 . . . . . 6 class (topGen‘𝑥)
9 vj . . . . . . 7 setvar 𝑗
109cv 1537 . . . . . 6 class 𝑗
118, 10wceq 1538 . . . . 5 wff (topGen‘𝑥) = 𝑗
126, 11wa 399 . . . 4 wff (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)
13 ctb 21553 . . . 4 class TopBases
1412, 2, 13wrex 3110 . . 3 wff 𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)
1514, 9cab 2779 . 2 class {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
161, 15wceq 1538 1 wff 2ndω = {𝑗 ∣ ∃𝑥 ∈ TopBases (𝑥 ≼ ω ∧ (topGen‘𝑥) = 𝑗)}
Colors of variables: wff setvar class
This definition is referenced by:  is2ndc  22054
  Copyright terms: Public domain W3C validator