Description: The singleton of the empty set is the only topology possible for an empty underlying set. (Contributed by NM, 9-Sep-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | 0top | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | olc | |
|
2 | 0opn | |
|
3 | n0i | |
|
4 | 2 3 | syl | |
5 | 4 | pm2.21d | |
6 | idd | |
|
7 | 5 6 | jaod | |
8 | 1 7 | impbid2 | |
9 | uni0b | |
|
10 | sssn | |
|
11 | 9 10 | bitr2i | |
12 | 8 11 | bitr2di | |