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

Definition df-top 21432
Description: Define the class of topologies. It is a proper class (see topnex 21534). See istopg 21433 and istop2g 21434 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 = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥 𝑦𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ∈ 𝑥)}
Distinct variable group:   𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-top
StepHypRef Expression
1 ctop 21431 . 2 class Top
2 vy . . . . . . . 8 setvar 𝑦
32cv 1527 . . . . . . 7 class 𝑦
43cuni 4832 . . . . . 6 class 𝑦
5 vx . . . . . . 7 setvar 𝑥
65cv 1527 . . . . . 6 class 𝑥
74, 6wcel 2105 . . . . 5 wff 𝑦𝑥
86cpw 4537 . . . . 5 class 𝒫 𝑥
97, 2, 8wral 3138 . . . 4 wff 𝑦 ∈ 𝒫 𝑥 𝑦𝑥
10 vz . . . . . . . . 9 setvar 𝑧
1110cv 1527 . . . . . . . 8 class 𝑧
123, 11cin 3934 . . . . . . 7 class (𝑦𝑧)
1312, 6wcel 2105 . . . . . 6 wff (𝑦𝑧) ∈ 𝑥
1413, 10, 6wral 3138 . . . . 5 wff 𝑧𝑥 (𝑦𝑧) ∈ 𝑥
1514, 2, 6wral 3138 . . . 4 wff 𝑦𝑥𝑧𝑥 (𝑦𝑧) ∈ 𝑥
169, 15wa 396 . . 3 wff (∀𝑦 ∈ 𝒫 𝑥 𝑦𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ∈ 𝑥)
1716, 5cab 2799 . 2 class {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥 𝑦𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ∈ 𝑥)}
181, 17wceq 1528 1 wff Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥 𝑦𝑥 ∧ ∀𝑦𝑥𝑧𝑥 (𝑦𝑧) ∈ 𝑥)}
Colors of variables: wff setvar class
This definition is referenced by:  istopg  21433
  Copyright terms: Public domain W3C validator