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

Definition df-top 16636
Description: Define the (proper) class of all topologies. See istop2g 16642 for an alternate way to express finite intersection and istps5OLD 16662 for a standard definition in terms of both members of a topological space. (Contributed by NM, 3-Mar-2006.)
Assertion
Ref Expression
df-top  |-  Top  =  { x  |  ( A. y  e.  ~P  x U. y  e.  x  /\  A. y  e.  x  A. z  e.  x  ( y  i^i  z
)  e.  x ) }
Distinct variable group:    x, y, z

Detailed syntax breakdown of Definition df-top
StepHypRef Expression
1 ctop 16631 . 2  class  Top
2 vy . . . . . . . 8  set  y
32cv 1622 . . . . . . 7  class  y
43cuni 3827 . . . . . 6  class  U. y
5 vx . . . . . . 7  set  x
65cv 1622 . . . . . 6  class  x
74, 6wcel 1684 . . . . 5  wff  U. y  e.  x
86cpw 3625 . . . . 5  class  ~P x
97, 2, 8wral 2543 . . . 4  wff  A. y  e.  ~P  x U. y  e.  x
10 vz . . . . . . . . 9  set  z
1110cv 1622 . . . . . . . 8  class  z
123, 11cin 3151 . . . . . . 7  class  ( y  i^i  z )
1312, 6wcel 1684 . . . . . 6  wff  ( y  i^i  z )  e.  x
1413, 10, 6wral 2543 . . . . 5  wff  A. z  e.  x  ( y  i^i  z )  e.  x
1514, 2, 6wral 2543 . . . 4  wff  A. y  e.  x  A. z  e.  x  ( y  i^i  z )  e.  x
169, 15wa 358 . . 3  wff  ( A. y  e.  ~P  x U. y  e.  x  /\  A. y  e.  x  A. z  e.  x  ( y  i^i  z
)  e.  x )
1716, 5cab 2269 . 2  class  { x  |  ( A. y  e.  ~P  x U. y  e.  x  /\  A. y  e.  x  A. z  e.  x  ( y  i^i  z )  e.  x
) }
181, 17wceq 1623 1  wff  Top  =  { x  |  ( A. y  e.  ~P  x U. y  e.  x  /\  A. y  e.  x  A. z  e.  x  ( y  i^i  z
)  e.  x ) }
Colors of variables: wff set class
This definition is referenced by:  istopg  16641
  Copyright terms: Public domain W3C validator