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

Definition df-top 12202
Description: Define the class of topologies. It is a proper class. See istopg 12203 and istopfin 12204 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 12201 . 2  class  Top
2 vy . . . . . . . 8  setvar  y
32cv 1331 . . . . . . 7  class  y
43cuni 3743 . . . . . 6  class  U. y
5 vx . . . . . . 7  setvar  x
65cv 1331 . . . . . 6  class  x
74, 6wcel 1481 . . . . 5  wff  U. y  e.  x
86cpw 3514 . . . . 5  class  ~P x
97, 2, 8wral 2417 . . . 4  wff  A. y  e.  ~P  x U. y  e.  x
10 vz . . . . . . . . 9  setvar  z
1110cv 1331 . . . . . . . 8  class  z
123, 11cin 3074 . . . . . . 7  class  ( y  i^i  z )
1312, 6wcel 1481 . . . . . 6  wff  ( y  i^i  z )  e.  x
1413, 10, 6wral 2417 . . . . 5  wff  A. z  e.  x  ( y  i^i  z )  e.  x
1514, 2, 6wral 2417 . . . 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 2126 . 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 1332 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  12203
  Copyright terms: Public domain W3C validator