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

Definition df-top 11947
Description: Define the class of topologies. It is a proper class. See istopg 11948 and istopfin 11949 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 11946 . 2  class  Top
2 vy . . . . . . . 8  setvar  y
32cv 1298 . . . . . . 7  class  y
43cuni 3683 . . . . . 6  class  U. y
5 vx . . . . . . 7  setvar  x
65cv 1298 . . . . . 6  class  x
74, 6wcel 1448 . . . . 5  wff  U. y  e.  x
86cpw 3457 . . . . 5  class  ~P x
97, 2, 8wral 2375 . . . 4  wff  A. y  e.  ~P  x U. y  e.  x
10 vz . . . . . . . . 9  setvar  z
1110cv 1298 . . . . . . . 8  class  z
123, 11cin 3020 . . . . . . 7  class  ( y  i^i  z )
1312, 6wcel 1448 . . . . . 6  wff  ( y  i^i  z )  e.  x
1413, 10, 6wral 2375 . . . . 5  wff  A. z  e.  x  ( y  i^i  z )  e.  x
1514, 2, 6wral 2375 . . . 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 2086 . 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 1299 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  11948
  Copyright terms: Public domain W3C validator