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 u. { (/) } )
Assertion ufildr 
|- ( F e. ( UFil ` X ) -> ( J u. ( Clsd ` J ) ) = ~P X )

Proof

Step Hyp Ref Expression
1 ufildr.1 
 |-  J = ( F u. { (/) } )
2 elssuni 
 |-  ( x e. J -> x C_ U. J )
3 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
4 filunibas 
 |-  ( F e. ( Fil ` X ) -> U. F = X )
5 3 4 syl 
 |-  ( F e. ( UFil ` X ) -> U. F = X )
6 1 unieqi 
 |-  U. J = U. ( F u. { (/) } )
7 uniun 
 |-  U. ( F u. { (/) } ) = ( U. F u. U. { (/) } )
8 0ex 
 |-  (/) e. _V
9 8 unisn 
 |-  U. { (/) } = (/)
10 9 uneq2i 
 |-  ( U. F u. U. { (/) } ) = ( U. F u. (/) )
11 un0 
 |-  ( U. F u. (/) ) = U. F
12 7 10 11 3eqtri 
 |-  U. ( F u. { (/) } ) = U. F
13 6 12 eqtr2i 
 |-  U. F = U. J
14 5 13 eqtr3di 
 |-  ( F e. ( UFil ` X ) -> X = U. J )
15 14 sseq2d 
 |-  ( F e. ( UFil ` X ) -> ( x C_ X <-> x C_ U. J ) )
16 2 15 imbitrrid 
 |-  ( F e. ( UFil ` X ) -> ( x e. J -> x C_ X ) )
17 eqid 
 |-  U. J = U. J
18 17 cldss 
 |-  ( x e. ( Clsd ` J ) -> x C_ U. J )
19 18 15 imbitrrid 
 |-  ( F e. ( UFil ` X ) -> ( x e. ( Clsd ` J ) -> x C_ X ) )
20 16 19 jaod 
 |-  ( F e. ( UFil ` X ) -> ( ( x e. J \/ x e. ( Clsd ` J ) ) -> x C_ X ) )
21 ufilss 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( x e. F \/ ( X \ x ) e. F ) )
22 ssun1 
 |-  F C_ ( F u. { (/) } )
23 22 1 sseqtrri 
 |-  F C_ J
24 23 a1i 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> F C_ J )
25 24 sseld 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( x e. F -> x e. J ) )
26 24 sseld 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( ( X \ x ) e. F -> ( X \ x ) e. J ) )
27 filconn 
 |-  ( F e. ( Fil ` X ) -> ( F u. { (/) } ) e. Conn )
28 conntop 
 |-  ( ( F u. { (/) } ) e. Conn -> ( F u. { (/) } ) e. Top )
29 3 27 28 3syl 
 |-  ( F e. ( UFil ` X ) -> ( F u. { (/) } ) e. Top )
30 1 29 eqeltrid 
 |-  ( F e. ( UFil ` X ) -> J e. Top )
31 15 biimpa 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> x C_ U. J )
32 17 iscld2 
 |-  ( ( J e. Top /\ x C_ U. J ) -> ( x e. ( Clsd ` J ) <-> ( U. J \ x ) e. J ) )
33 30 31 32 syl2an2r 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( x e. ( Clsd ` J ) <-> ( U. J \ x ) e. J ) )
34 14 difeq1d 
 |-  ( F e. ( UFil ` X ) -> ( X \ x ) = ( U. J \ x ) )
35 34 eleq1d 
 |-  ( F e. ( UFil ` X ) -> ( ( X \ x ) e. J <-> ( U. J \ x ) e. J ) )
36 35 adantr 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( ( X \ x ) e. J <-> ( U. J \ x ) e. J ) )
37 33 36 bitr4d 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( x e. ( Clsd ` J ) <-> ( X \ x ) e. J ) )
38 26 37 sylibrd 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( ( X \ x ) e. F -> x e. ( Clsd ` J ) ) )
39 25 38 orim12d 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( ( x e. F \/ ( X \ x ) e. F ) -> ( x e. J \/ x e. ( Clsd ` J ) ) ) )
40 21 39 mpd 
 |-  ( ( F e. ( UFil ` X ) /\ x C_ X ) -> ( x e. J \/ x e. ( Clsd ` J ) ) )
41 40 ex 
 |-  ( F e. ( UFil ` X ) -> ( x C_ X -> ( x e. J \/ x e. ( Clsd ` J ) ) ) )
42 20 41 impbid 
 |-  ( F e. ( UFil ` X ) -> ( ( x e. J \/ x e. ( Clsd ` J ) ) <-> x C_ X ) )
43 elun 
 |-  ( x e. ( J u. ( Clsd ` J ) ) <-> ( x e. J \/ x e. ( Clsd ` J ) ) )
44 velpw 
 |-  ( x e. ~P X <-> x C_ X )
45 42 43 44 3bitr4g 
 |-  ( F e. ( UFil ` X ) -> ( x e. ( J u. ( Clsd ` J ) ) <-> x e. ~P X ) )
46 45 eqrdv 
 |-  ( F e. ( UFil ` X ) -> ( J u. ( Clsd ` J ) ) = ~P X )