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

Definition df-1stc 19062
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 19060 . 2  class  1stc
2 vy . . . . . . . 8  setvar  y
32cv 1368 . . . . . . 7  class  y
4 com 6495 . . . . . . 7  class  om
5 cdom 7327 . . . . . . 7  class  ~<_
63, 4, 5wbr 4311 . . . . . 6  wff  y  ~<_  om
7 vx . . . . . . . . 9  setvar  x
8 vz . . . . . . . . 9  setvar  z
97, 8wel 1757 . . . . . . . 8  wff  x  e.  z
107cv 1368 . . . . . . . . 9  class  x
118cv 1368 . . . . . . . . . . . 12  class  z
1211cpw 3879 . . . . . . . . . . 11  class  ~P z
133, 12cin 3346 . . . . . . . . . 10  class  ( y  i^i  ~P z )
1413cuni 4110 . . . . . . . . 9  class  U. (
y  i^i  ~P z
)
1510, 14wcel 1756 . . . . . . . 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  setvar  j
1817cv 1368 . . . . . . 7  class  j
1916, 8, 18wral 2734 . . . . . 6  wff  A. z  e.  j  ( x  e.  z  ->  x  e. 
U. ( y  i^i 
~P z ) )
206, 19wa 369 . . . . 5  wff  ( y  ~<_  om  /\  A. z  e.  j  ( x  e.  z  ->  x  e. 
U. ( y  i^i 
~P z ) ) )
2118cpw 3879 . . . . 5  class  ~P j
2220, 2, 21wrex 2735 . . . 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 4110 . . . 4  class  U. j
2422, 7, 23wral 2734 . . 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 18517 . . 3  class  Top
2624, 17, 25crab 2738 . 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 1369 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 setvar class
This definition is referenced by:  is1stc  19064
  Copyright terms: Public domain W3C validator