This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( 𝐹 ∪ { ∅ } )
Assertion ufildr ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 ∪ ( Clsd ‘ 𝐽 ) ) = 𝒫 𝑋 )

Proof

Step Hyp Ref Expression
1 ufildr.1 ⊢ 𝐽 = ( 𝐹 ∪ { ∅ } )
2 elssuni ⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 )
3 ufilfil ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
4 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
5 3 4 syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
6 1 unieqi ⊢ ∪ 𝐽 = ∪ ( 𝐹 ∪ { ∅ } )
7 uniun ⊢ ∪ ( 𝐹 ∪ { ∅ } ) = ( ∪ 𝐹 ∪ ∪ { ∅ } )
8 0ex ⊢ ∅ ∈ V
9 8 unisn ⊢ ∪ { ∅ } = ∅
10 9 uneq2i ⊢ ( ∪ 𝐹 ∪ ∪ { ∅ } ) = ( ∪ 𝐹 ∪ ∅ )
11 un0 ⊢ ( ∪ 𝐹 ∪ ∅ ) = ∪ 𝐹
12 7 10 11 3eqtri ⊢ ∪ ( 𝐹 ∪ { ∅ } ) = ∪ 𝐹
13 6 12 eqtr2i ⊢ ∪ 𝐹 = ∪ 𝐽
14 5 13 eqtr3di ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
15 14 sseq2d ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ⊆ 𝑋 ↔ 𝑥 ⊆ ∪ 𝐽 ) )
16 2 15 imbitrrid ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ 𝑋 ) )
17 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
18 17 cldss ⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ ∪ 𝐽 )
19 18 15 imbitrrid ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ 𝑋 ) )
20 16 19 jaod ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑥 ⊆ 𝑋 ) )
21 ufilss ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) )
22 ssun1 ⊢ 𝐹 ⊆ ( 𝐹 ∪ { ∅ } )
23 22 1 sseqtrri ⊢ 𝐹 ⊆ 𝐽
24 23 a1i ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝐹 ⊆ 𝐽 )
25 24 sseld ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐹 → 𝑥 ∈ 𝐽 ) )
26 24 sseld ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ) )
27 filconn ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ { ∅ } ) ∈ Conn )
28 conntop ⊢ ( ( 𝐹 ∪ { ∅ } ) ∈ Conn → ( 𝐹 ∪ { ∅ } ) ∈ Top )
29 3 27 28 3syl ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐹 ∪ { ∅ } ) ∈ Top )
30 1 29 eqeltrid ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → 𝐽 ∈ Top )
31 15 biimpa ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → 𝑥 ⊆ ∪ 𝐽 )
32 17 iscld2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ⊆ ∪ 𝐽 ) → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) )
33 30 31 32 syl2an2r ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) )
34 14 difeq1d ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑋 ∖ 𝑥 ) = ( ∪ 𝐽 ∖ 𝑥 ) )
35 34 eleq1d ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ↔ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) )
36 35 adantr ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ↔ ( ∪ 𝐽 ∖ 𝑥 ) ∈ 𝐽 ) )
37 33 36 bitr4d ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐽 ) )
38 26 37 sylibrd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 → 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
39 25 38 orim12d ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) → ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) )
40 21 39 mpd ⊢ ( ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
41 40 ex ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ⊆ 𝑋 → ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ) )
42 20 41 impbid ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) ↔ 𝑥 ⊆ 𝑋 ) )
43 elun ⊢ ( 𝑥 ∈ ( 𝐽 ∪ ( Clsd ‘ 𝐽 ) ) ↔ ( 𝑥 ∈ 𝐽 ∨ 𝑥 ∈ ( Clsd ‘ 𝐽 ) ) )
44 velpw ⊢ ( 𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋 )
45 42 43 44 3bitr4g ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝑥 ∈ ( 𝐽 ∪ ( Clsd ‘ 𝐽 ) ) ↔ 𝑥 ∈ 𝒫 𝑋 ) )
46 45 eqrdv ⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) → ( 𝐽 ∪ ( Clsd ‘ 𝐽 ) ) = 𝒫 𝑋 )