![]() |
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 22917).
See istopg 22815 and istop2g 22816 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 22813 | . 2 class Top | |
2 | vy | . . . . . . . 8 setvar 𝑦 | |
3 | 2 | cv 1532 | . . . . . . 7 class 𝑦 |
4 | 3 | cuni 4910 | . . . . . 6 class ∪ 𝑦 |
5 | vx | . . . . . . 7 setvar 𝑥 | |
6 | 5 | cv 1532 | . . . . . 6 class 𝑥 |
7 | 4, 6 | wcel 2098 | . . . . 5 wff ∪ 𝑦 ∈ 𝑥 |
8 | 6 | cpw 4604 | . . . . 5 class 𝒫 𝑥 |
9 | 7, 2, 8 | wral 3057 | . . . 4 wff ∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 |
10 | vz | . . . . . . . . 9 setvar 𝑧 | |
11 | 10 | cv 1532 | . . . . . . . 8 class 𝑧 |
12 | 3, 11 | cin 3946 | . . . . . . 7 class (𝑦 ∩ 𝑧) |
13 | 12, 6 | wcel 2098 | . . . . . 6 wff (𝑦 ∩ 𝑧) ∈ 𝑥 |
14 | 13, 10, 6 | wral 3057 | . . . . 5 wff ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
15 | 14, 2, 6 | wral 3057 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
16 | 9, 15 | wa 394 | . . 3 wff (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥) |
17 | 16, 5 | cab 2704 | . 2 class {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
18 | 1, 17 | wceq 1533 | 1 wff Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
Colors of variables: wff setvar class |
This definition is referenced by: istopg 22815 |
Copyright terms: Public domain | W3C validator |