Metamath Proof Explorer


Theorem ufildr

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 J=F
Assertion ufildr FUFilXJClsdJ=𝒫X

Proof

Step Hyp Ref Expression
1 ufildr.1 J=F
2 elssuni xJxJ
3 ufilfil FUFilXFFilX
4 filunibas FFilXF=X
5 3 4 syl FUFilXF=X
6 1 unieqi J=F
7 uniun F=F
8 0ex V
9 8 unisn =
10 9 uneq2i F=F
11 un0 F=F
12 7 10 11 3eqtri F=F
13 6 12 eqtr2i F=J
14 5 13 eqtr3di FUFilXX=J
15 14 sseq2d FUFilXxXxJ
16 2 15 syl5ibr FUFilXxJxX
17 eqid J=J
18 17 cldss xClsdJxJ
19 18 15 syl5ibr FUFilXxClsdJxX
20 16 19 jaod FUFilXxJxClsdJxX
21 ufilss FUFilXxXxFXxF
22 ssun1 FF
23 22 1 sseqtrri FJ
24 23 a1i FUFilXxXFJ
25 24 sseld FUFilXxXxFxJ
26 24 sseld FUFilXxXXxFXxJ
27 filconn FFilXFConn
28 conntop FConnFTop
29 3 27 28 3syl FUFilXFTop
30 1 29 eqeltrid FUFilXJTop
31 15 biimpa FUFilXxXxJ
32 17 iscld2 JTopxJxClsdJJxJ
33 30 31 32 syl2an2r FUFilXxXxClsdJJxJ
34 14 difeq1d FUFilXXx=Jx
35 34 eleq1d FUFilXXxJJxJ
36 35 adantr FUFilXxXXxJJxJ
37 33 36 bitr4d FUFilXxXxClsdJXxJ
38 26 37 sylibrd FUFilXxXXxFxClsdJ
39 25 38 orim12d FUFilXxXxFXxFxJxClsdJ
40 21 39 mpd FUFilXxXxJxClsdJ
41 40 ex FUFilXxXxJxClsdJ
42 20 41 impbid FUFilXxJxClsdJxX
43 elun xJClsdJxJxClsdJ
44 velpw x𝒫XxX
45 42 43 44 3bitr4g FUFilXxJClsdJx𝒫X
46 45 eqrdv FUFilXJClsdJ=𝒫X