Description: An ultrafilter gives rise to a connected door topology. (Contributed by Jeff Hankins, 6-Dec-2009) (Revised by Stefan O'Rear, 3-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ufildr.1 | |
|
Assertion | ufildr | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ufildr.1 | |
|
2 | elssuni | |
|
3 | ufilfil | |
|
4 | filunibas | |
|
5 | 3 4 | syl | |
6 | 1 | unieqi | |
7 | uniun | |
|
8 | 0ex | |
|
9 | 8 | unisn | |
10 | 9 | uneq2i | |
11 | un0 | |
|
12 | 7 10 11 | 3eqtri | |
13 | 6 12 | eqtr2i | |
14 | 5 13 | eqtr3di | |
15 | 14 | sseq2d | |
16 | 2 15 | syl5ibr | |
17 | eqid | |
|
18 | 17 | cldss | |
19 | 18 15 | syl5ibr | |
20 | 16 19 | jaod | |
21 | ufilss | |
|
22 | ssun1 | |
|
23 | 22 1 | sseqtrri | |
24 | 23 | a1i | |
25 | 24 | sseld | |
26 | 24 | sseld | |
27 | filconn | |
|
28 | conntop | |
|
29 | 3 27 28 | 3syl | |
30 | 1 29 | eqeltrid | |
31 | 15 | biimpa | |
32 | 17 | iscld2 | |
33 | 30 31 32 | syl2an2r | |
34 | 14 | difeq1d | |
35 | 34 | eleq1d | |
36 | 35 | adantr | |
37 | 33 36 | bitr4d | |
38 | 26 37 | sylibrd | |
39 | 25 38 | orim12d | |
40 | 21 39 | mpd | |
41 | 40 | ex | |
42 | 20 41 | impbid | |
43 | elun | |
|
44 | velpw | |
|
45 | 42 43 44 | 3bitr4g | |
46 | 45 | eqrdv | |