| 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 23003).
See istopg 22901 and istop2g 22902 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 22899 | . 2 class Top | |
| 2 | vy | . . . . . . . 8 setvar 𝑦 | |
| 3 | 2 | cv 1539 | . . . . . . 7 class 𝑦 |
| 4 | 3 | cuni 4907 | . . . . . 6 class ∪ 𝑦 |
| 5 | vx | . . . . . . 7 setvar 𝑥 | |
| 6 | 5 | cv 1539 | . . . . . 6 class 𝑥 |
| 7 | 4, 6 | wcel 2108 | . . . . 5 wff ∪ 𝑦 ∈ 𝑥 |
| 8 | 6 | cpw 4600 | . . . . 5 class 𝒫 𝑥 |
| 9 | 7, 2, 8 | wral 3061 | . . . 4 wff ∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 |
| 10 | vz | . . . . . . . . 9 setvar 𝑧 | |
| 11 | 10 | cv 1539 | . . . . . . . 8 class 𝑧 |
| 12 | 3, 11 | cin 3950 | . . . . . . 7 class (𝑦 ∩ 𝑧) |
| 13 | 12, 6 | wcel 2108 | . . . . . 6 wff (𝑦 ∩ 𝑧) ∈ 𝑥 |
| 14 | 13, 10, 6 | wral 3061 | . . . . 5 wff ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
| 15 | 14, 2, 6 | wral 3061 | . . . 4 wff ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥 |
| 16 | 9, 15 | wa 395 | . . 3 wff (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥) |
| 17 | 16, 5 | cab 2714 | . 2 class {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
| 18 | 1, 17 | wceq 1540 | 1 wff Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} |
| Colors of variables: wff setvar class |
| This definition is referenced by: istopg 22901 |
| Copyright terms: Public domain | W3C validator |