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

Definition df-top 18483
Description: Define the (proper) class of all topologies. See istop2g 18489 for an alternate way to express finite intersection and istps5OLD 18509 for a standard definition as an ordered pair of a set and a topology on it.

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
Distinct variable group:   , ,

Detailed syntax breakdown of Definition df-top
StepHypRef Expression
1 ctop 18478 . 2
2 vy . . . . . . . 8
32cv 1368 . . . . . . 7
43cuni 4086 . . . . . 6
5 vx . . . . . . 7
65cv 1368 . . . . . 6
74, 6wcel 1756 . . . . 5
86cpw 3855 . . . . 5
97, 2, 8wral 2710 . . . 4
10 vz . . . . . . . . 9
1110cv 1368 . . . . . . . 8
123, 11cin 3322 . . . . . . 7
1312, 6wcel 1756 . . . . . 6
1413, 10, 6wral 2710 . . . . 5
1514, 2, 6wral 2710 . . . 4
169, 15wa 369 . . 3
1716, 5cab 2424 . 2
181, 17wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  istopg  18488
  Copyright terms: Public domain W3C validator