Description: If a topology has two elements, it is the indiscrete topology. (Contributed by FL, 11-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | en2top | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr | |
|
2 | toponss | |
|
3 | 2 | ad2ant2rl | |
4 | simprl | |
|
5 | sseq0 | |
|
6 | 3 4 5 | syl2anc | |
7 | velsn | |
|
8 | 6 7 | sylibr | |
9 | 8 | expr | |
10 | 9 | ssrdv | |
11 | topontop | |
|
12 | 0opn | |
|
13 | 11 12 | syl | |
14 | 13 | ad2antrr | |
15 | 14 | snssd | |
16 | 10 15 | eqssd | |
17 | 0ex | |
|
18 | 17 | ensn1 | |
19 | 16 18 | eqbrtrdi | |
20 | 19 | olcd | |
21 | sdom2en01 | |
|
22 | 20 21 | sylibr | |
23 | sdomnen | |
|
24 | 22 23 | syl | |
25 | 24 | ex | |
26 | 25 | necon2ad | |
27 | 1 26 | mpd | |
28 | 27 | necomd | |
29 | 13 | adantr | |
30 | toponmax | |
|
31 | 30 | adantr | |
32 | en2eqpr | |
|
33 | 1 29 31 32 | syl3anc | |
34 | 28 33 | mpd | |
35 | 34 27 | jca | |
36 | simprl | |
|
37 | simprr | |
|
38 | 37 | necomd | |
39 | pr2nelem | |
|
40 | 17 30 38 39 | mp3an2ani | |
41 | 36 40 | eqbrtrd | |
42 | 35 41 | impbida | |