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 12538 and
istopfin 12539 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 12536 | . 2 | |
2 | vy | . . . . . . . 8 | |
3 | 2 | cv 1341 | . . . . . . 7 |
4 | 3 | cuni 3783 | . . . . . 6 |
5 | vx | . . . . . . 7 | |
6 | 5 | cv 1341 | . . . . . 6 |
7 | 4, 6 | wcel 2135 | . . . . 5 |
8 | 6 | cpw 3553 | . . . . 5 |
9 | 7, 2, 8 | wral 2442 | . . . 4 |
10 | vz | . . . . . . . . 9 | |
11 | 10 | cv 1341 | . . . . . . . 8 |
12 | 3, 11 | cin 3110 | . . . . . . 7 |
13 | 12, 6 | wcel 2135 | . . . . . 6 |
14 | 13, 10, 6 | wral 2442 | . . . . 5 |
15 | 14, 2, 6 | wral 2442 | . . . 4 |
16 | 9, 15 | wa 103 | . . 3 |
17 | 16, 5 | cab 2150 | . 2 |
18 | 1, 17 | wceq 1342 | 1 |
Colors of variables: wff set class |
This definition is referenced by: istopg 12538 |
Copyright terms: Public domain | W3C validator |