![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-top | Structured version Visualization version GIF version |
Description: Define the class of
topologies. It is a proper class (see topnex 23018).
See istopg 22916 and istop2g 22917 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.) |
Ref | Expression |
---|---|
df-top | ⊢ Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ctop 22914 | . 2 class Top | |
2 | vy | . . . . . . . 8 setvar 𝑦 | |
3 | 2 | cv 1535 | . . . . . . 7 class 𝑦 |
4 | 3 | cuni 4911 | . . . . . 6 class ∪ 𝑦 |
5 | vx | . . . . . . 7 setvar 𝑥 | |
6 | 5 | cv 1535 | . . . . . 6 class 𝑥 |
7 | 4, 6 | wcel 2105 | . . . . 5 wff ∪ 𝑦 ∈ 𝑥 |
8 | 6 | cpw 4604 | . . . . 5 class 𝒫 𝑥 |
9 | 7, 2, 8 | wral 3058 | . . . 4 wff ∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 |
10 | vz | . . . . . . . . 9 setvar 𝑧 | |
11 | 10 | cv 1535 | . . . . . . . 8 class 𝑧 |
12 | 3, 11 | cin 3961 | . . . . . . 7 class (𝑦 ∩ 𝑧) |
13 | 12, 6 | wcel 2105 | . . . . . 6 wff (𝑦 ∩ 𝑧) ∈ 𝑥 |
14 | 13, 10, 6 | wral 3058 | . . . . 5 wff ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
15 | 14, 2, 6 | wral 3058 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
16 | 9, 15 | wa 395 | . . 3 wff (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥) |
17 | 16, 5 | cab 2711 | . 2 class {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
18 | 1, 17 | wceq 1536 | 1 wff Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
Colors of variables: wff setvar class |
This definition is referenced by: istopg 22916 |
Copyright terms: Public domain | W3C validator |