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

Definition df-2ndc 17166
Description: Define the class of all second-countable topologies. (Contributed by Jeff Hankins, 17-Jan-2010.)
Assertion
Ref Expression
df-2ndc  |-  2ndc  =  { j  |  E. x  e.  TopBases  ( x  ~<_  om  /\  ( topGen `  x
)  =  j ) }
Distinct variable group:    x, j

Detailed syntax breakdown of Definition df-2ndc
StepHypRef Expression
1 c2ndc 17164 . 2  class  2ndc
2 vx . . . . . . 7  set  x
32cv 1622 . . . . . 6  class  x
4 com 4656 . . . . . 6  class  om
5 cdom 6861 . . . . . 6  class  ~<_
63, 4, 5wbr 4023 . . . . 5  wff  x  ~<_  om
7 ctg 13342 . . . . . . 7  class  topGen
83, 7cfv 5255 . . . . . 6  class  ( topGen `  x )
9 vj . . . . . . 7  set  j
109cv 1622 . . . . . 6  class  j
118, 10wceq 1623 . . . . 5  wff  ( topGen `  x )  =  j
126, 11wa 358 . . . 4  wff  ( x  ~<_  om  /\  ( topGen `  x )  =  j )
13 ctb 16635 . . . 4  class  TopBases
1412, 2, 13wrex 2544 . . 3  wff  E. x  e. 
TopBases  ( x  ~<_  om  /\  ( topGen `  x )  =  j )
1514, 9cab 2269 . 2  class  { j  |  E. x  e.  TopBases  ( x  ~<_  om  /\  ( topGen `  x )  =  j ) }
161, 15wceq 1623 1  wff  2ndc  =  { j  |  E. x  e.  TopBases  ( x  ~<_  om  /\  ( topGen `  x
)  =  j ) }
Colors of variables: wff set class
This definition is referenced by:  is2ndc  17172
  Copyright terms: Public domain W3C validator