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

Definition df-1stc 17181
Description: Define the class of all first-countable topologies. (Contributed by Jeff Hankins, 22-Aug-2009.)
Assertion
Ref Expression
df-1stc  |-  1stc  =  { j  e.  Top  | 
A. x  e.  U. j E. y  e.  ~P  j ( y  ~<_  om 
/\  A. z  e.  j  ( x  e.  z  ->  x  e.  U. ( y  i^i  ~P z ) ) ) }
Distinct variable group:    x, j, y, z

Detailed syntax breakdown of Definition df-1stc
StepHypRef Expression
1 c1stc 17179 . 2  class  1stc
2 vy . . . . . . . 8  set  y
32cv 1631 . . . . . . 7  class  y
4 com 4672 . . . . . . 7  class  om
5 cdom 6877 . . . . . . 7  class  ~<_
63, 4, 5wbr 4039 . . . . . 6  wff  y  ~<_  om
7 vx . . . . . . . . 9  set  x
8 vz . . . . . . . . 9  set  z
97, 8wel 1697 . . . . . . . 8  wff  x  e.  z
107cv 1631 . . . . . . . . 9  class  x
118cv 1631 . . . . . . . . . . . 12  class  z
1211cpw 3638 . . . . . . . . . . 11  class  ~P z
133, 12cin 3164 . . . . . . . . . 10  class  ( y  i^i  ~P z )
1413cuni 3843 . . . . . . . . 9  class  U. (
y  i^i  ~P z
)
1510, 14wcel 1696 . . . . . . . 8  wff  x  e. 
U. ( y  i^i 
~P z )
169, 15wi 4 . . . . . . 7  wff  ( x  e.  z  ->  x  e.  U. ( y  i^i 
~P z ) )
17 vj . . . . . . . 8  set  j
1817cv 1631 . . . . . . 7  class  j
1916, 8, 18wral 2556 . . . . . 6  wff  A. z  e.  j  ( x  e.  z  ->  x  e. 
U. ( y  i^i 
~P z ) )
206, 19wa 358 . . . . 5  wff  ( y  ~<_  om  /\  A. z  e.  j  ( x  e.  z  ->  x  e. 
U. ( y  i^i 
~P z ) ) )
2118cpw 3638 . . . . 5  class  ~P j
2220, 2, 21wrex 2557 . . . 4  wff  E. y  e.  ~P  j ( y  ~<_  om  /\  A. z  e.  j  ( x  e.  z  ->  x  e. 
U. ( y  i^i 
~P z ) ) )
2318cuni 3843 . . . 4  class  U. j
2422, 7, 23wral 2556 . . 3  wff  A. x  e.  U. j E. y  e.  ~P  j ( y  ~<_  om  /\  A. z  e.  j  ( x  e.  z  ->  x  e. 
U. ( y  i^i 
~P z ) ) )
25 ctop 16647 . . 3  class  Top
2624, 17, 25crab 2560 . 2  class  { j  e.  Top  |  A. x  e.  U. j E. y  e.  ~P  j ( y  ~<_  om 
/\  A. z  e.  j  ( x  e.  z  ->  x  e.  U. ( y  i^i  ~P z ) ) ) }
271, 26wceq 1632 1  wff  1stc  =  { j  e.  Top  | 
A. x  e.  U. j E. y  e.  ~P  j ( y  ~<_  om 
/\  A. z  e.  j  ( x  e.  z  ->  x  e.  U. ( y  i^i  ~P z ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  is1stc  17183
  Copyright terms: Public domain W3C validator