Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-top | Structured version Visualization version GIF version |
Description: Define the (proper) class
of all topologies. See istop2g 20526 for an
alternate way to express finite intersection.
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 20517 | . 2 class Top | |
2 | vy | . . . . . . . 8 setvar 𝑦 | |
3 | 2 | cv 1474 | . . . . . . 7 class 𝑦 |
4 | 3 | cuni 4372 | . . . . . 6 class ∪ 𝑦 |
5 | vx | . . . . . . 7 setvar 𝑥 | |
6 | 5 | cv 1474 | . . . . . 6 class 𝑥 |
7 | 4, 6 | wcel 1977 | . . . . 5 wff ∪ 𝑦 ∈ 𝑥 |
8 | 6 | cpw 4108 | . . . . 5 class 𝒫 𝑥 |
9 | 7, 2, 8 | wral 2896 | . . . 4 wff ∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 |
10 | vz | . . . . . . . . 9 setvar 𝑧 | |
11 | 10 | cv 1474 | . . . . . . . 8 class 𝑧 |
12 | 3, 11 | cin 3539 | . . . . . . 7 class (𝑦 ∩ 𝑧) |
13 | 12, 6 | wcel 1977 | . . . . . 6 wff (𝑦 ∩ 𝑧) ∈ 𝑥 |
14 | 13, 10, 6 | wral 2896 | . . . . 5 wff ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
15 | 14, 2, 6 | wral 2896 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
16 | 9, 15 | wa 383 | . . 3 wff (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥) |
17 | 16, 5 | cab 2596 | . 2 class {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
18 | 1, 17 | wceq 1475 | 1 wff Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
Colors of variables: wff setvar class |
This definition is referenced by: istopg 20525 |
Copyright terms: Public domain | W3C validator |