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

Definition df-top 16692
Description: Define the (proper) class of all topologies. See istop2g 16698 for an alternate way to express finite intersection and istps5OLD 16718 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 16687 . 2  class  Top
2 vy . . . . . . . 8  set  y
32cv 1632 . . . . . . 7  class  y
43cuni 3864 . . . . . 6  class  U. y
5 vx . . . . . . 7  set  x
65cv 1632 . . . . . 6  class  x
74, 6wcel 1701 . . . . 5  wff  U. y  e.  x
86cpw 3659 . . . . 5  class  ~P x
97, 2, 8wral 2577 . . . 4  wff  A. y  e.  ~P  x U. y  e.  x
10 vz . . . . . . . . 9  set  z
1110cv 1632 . . . . . . . 8  class  z
123, 11cin 3185 . . . . . . 7  class  ( y  i^i  z )
1312, 6wcel 1701 . . . . . 6  wff  ( y  i^i  z )  e.  x
1413, 10, 6wral 2577 . . . . 5  wff  A. z  e.  x  ( y  i^i  z )  e.  x
1514, 2, 6wral 2577 . . . 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 2302 . 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 1633 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  16697
  Copyright terms: Public domain W3C validator