Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-top | Unicode version |
Description: Define the class of
topologies. It is a proper class. See istopg 12166 and
istopfin 12167 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ctop 12164 | . 2 | |
2 | vy | . . . . . . . 8 | |
3 | 2 | cv 1330 | . . . . . . 7 |
4 | 3 | cuni 3736 | . . . . . 6 |
5 | vx | . . . . . . 7 | |
6 | 5 | cv 1330 | . . . . . 6 |
7 | 4, 6 | wcel 1480 | . . . . 5 |
8 | 6 | cpw 3510 | . . . . 5 |
9 | 7, 2, 8 | wral 2416 | . . . 4 |
10 | vz | . . . . . . . . 9 | |
11 | 10 | cv 1330 | . . . . . . . 8 |
12 | 3, 11 | cin 3070 | . . . . . . 7 |
13 | 12, 6 | wcel 1480 | . . . . . 6 |
14 | 13, 10, 6 | wral 2416 | . . . . 5 |
15 | 14, 2, 6 | wral 2416 | . . . 4 |
16 | 9, 15 | wa 103 | . . 3 |
17 | 16, 5 | cab 2125 | . 2 |
18 | 1, 17 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: istopg 12166 |
Copyright terms: Public domain | W3C validator |