![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-top | GIF version |
Description: Define the class of
topologies. It is a proper class. See istopg 12205 and
istopfin 12206 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 12203 | . 2 class Top | |
2 | vy | . . . . . . . 8 setvar 𝑦 | |
3 | 2 | cv 1331 | . . . . . . 7 class 𝑦 |
4 | 3 | cuni 3744 | . . . . . 6 class ∪ 𝑦 |
5 | vx | . . . . . . 7 setvar 𝑥 | |
6 | 5 | cv 1331 | . . . . . 6 class 𝑥 |
7 | 4, 6 | wcel 1481 | . . . . 5 wff ∪ 𝑦 ∈ 𝑥 |
8 | 6 | cpw 3515 | . . . . 5 class 𝒫 𝑥 |
9 | 7, 2, 8 | wral 2417 | . . . 4 wff ∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 |
10 | vz | . . . . . . . . 9 setvar 𝑧 | |
11 | 10 | cv 1331 | . . . . . . . 8 class 𝑧 |
12 | 3, 11 | cin 3075 | . . . . . . 7 class (𝑦 ∩ 𝑧) |
13 | 12, 6 | wcel 1481 | . . . . . 6 wff (𝑦 ∩ 𝑧) ∈ 𝑥 |
14 | 13, 10, 6 | wral 2417 | . . . . 5 wff ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
15 | 14, 2, 6 | wral 2417 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
16 | 9, 15 | wa 103 | . . 3 wff (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥) |
17 | 16, 5 | cab 2126 | . 2 class {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
18 | 1, 17 | wceq 1332 | 1 wff Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
Colors of variables: wff set class |
This definition is referenced by: istopg 12205 |
Copyright terms: Public domain | W3C validator |