ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-top Unicode version

Definition df-top 12711
Description: Define the class of topologies. It is a proper class. See istopg 12712 and istopfin 12713 for the corresponding characterizations, using respectively binary intersections like in this definition and nonempty finite intersections.

The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see

Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241.

(Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.)

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 12710 . 2  class  Top
2 vy . . . . . . . 8  setvar  y
32cv 1347 . . . . . . 7  class  y
43cuni 3794 . . . . . 6  class  U. y
5 vx . . . . . . 7  setvar  x
65cv 1347 . . . . . 6  class  x
74, 6wcel 2141 . . . . 5  wff  U. y  e.  x
86cpw 3564 . . . . 5  class  ~P x
97, 2, 8wral 2448 . . . 4  wff  A. y  e.  ~P  x U. y  e.  x
10 vz . . . . . . . . 9  setvar  z
1110cv 1347 . . . . . . . 8  class  z
123, 11cin 3120 . . . . . . 7  class  ( y  i^i  z )
1312, 6wcel 2141 . . . . . 6  wff  ( y  i^i  z )  e.  x
1413, 10, 6wral 2448 . . . . 5  wff  A. z  e.  x  ( y  i^i  z )  e.  x
1514, 2, 6wral 2448 . . . 4  wff  A. y  e.  x  A. z  e.  x  ( y  i^i  z )  e.  x
169, 15wa 103 . . 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 2156 . 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 1348 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  12712
  Copyright terms: Public domain W3C validator