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

Definition df-top 16631
Description: Define the (proper) class of all topologies. See istop2g 16637 for an alternate way to express finite intersection and istps5OLD 16657 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 16626 . 2  class  Top
2 vy . . . . . . . 8  set  y
32cv 1623 . . . . . . 7  class  y
43cuni 3829 . . . . . 6  class  U. y
5 vx . . . . . . 7  set  x
65cv 1623 . . . . . 6  class  x
74, 6wcel 1685 . . . . 5  wff  U. y  e.  x
86cpw 3627 . . . . 5  class  ~P x
97, 2, 8wral 2545 . . . 4  wff  A. y  e.  ~P  x U. y  e.  x
10 vz . . . . . . . . 9  set  z
1110cv 1623 . . . . . . . 8  class  z
123, 11cin 3153 . . . . . . 7  class  ( y  i^i  z )
1312, 6wcel 1685 . . . . . 6  wff  ( y  i^i  z )  e.  x
1413, 10, 6wral 2545 . . . . 5  wff  A. z  e.  x  ( y  i^i  z )  e.  x
1514, 2, 6wral 2545 . . . 4  wff  A. y  e.  x  A. z  e.  x  ( y  i^i  z )  e.  x
169, 15wa 360 . . 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 2271 . 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 1624 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  16636
  Copyright terms: Public domain W3C validator