Metamath Proof Explorer

Theorem filconn

Description: A filter gives rise to a connected topology. (Contributed by Jeff Hankins, 6-Dec-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion filconn ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ { ∅ } ) ∈ Conn )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ 𝑋 ) )
2 filunibas ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ∪ 𝐹 = 𝑋 )
3 2 fveq2d ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( Fil ‘ ∪ 𝐹 ) = ( Fil ‘ 𝑋 ) )
4 1 3 eleqtrrd ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
5 nss ⊢ ( ¬ 𝑥 ⊆ { ∅ } ↔ ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) )
6 simpll ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) )
7 ssel2 ⊢ ( ( 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) )
8 7 adantll ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) )
9 elun ⊢ ( 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ↔ ( 𝑦 ∈ 𝐹 ∨ 𝑦 ∈ { ∅ } ) )
10 8 9 sylib ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∈ 𝐹 ∨ 𝑦 ∈ { ∅ } ) )
11 10 orcomd ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ∈ { ∅ } ∨ 𝑦 ∈ 𝐹 ) )
12 11 ord ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ 𝑦 ∈ 𝑥 ) → ( ¬ 𝑦 ∈ { ∅ } → 𝑦 ∈ 𝐹 ) )
13 12 impr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) ) → 𝑦 ∈ 𝐹 )
14 uniss ⊢ ( 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) → ∪ 𝑥 ⊆ ∪ ( 𝐹 ∪ { ∅ } ) )
15 14 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) ) → ∪ 𝑥 ⊆ ∪ ( 𝐹 ∪ { ∅ } ) )
16 uniun ⊢ ∪ ( 𝐹 ∪ { ∅ } ) = ( ∪ 𝐹 ∪ ∪ { ∅ } )
17 0ex ⊢ ∅ ∈ V
18 17 unisn ⊢ ∪ { ∅ } = ∅
19 18 uneq2i ⊢ ( ∪ 𝐹 ∪ ∪ { ∅ } ) = ( ∪ 𝐹 ∪ ∅ )
20 un0 ⊢ ( ∪ 𝐹 ∪ ∅ ) = ∪ 𝐹
21 16 19 20 3eqtrri ⊢ ∪ 𝐹 = ∪ ( 𝐹 ∪ { ∅ } )
22 15 21 sseqtrrdi ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) ) → ∪ 𝑥 ⊆ ∪ 𝐹 )
23 elssuni ⊢ ( 𝑦 ∈ 𝑥 → 𝑦 ⊆ ∪ 𝑥 )
24 23 ad2antrl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) ) → 𝑦 ⊆ ∪ 𝑥 )
25 filss ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ ( 𝑦 ∈ 𝐹 ∧ ∪ 𝑥 ⊆ ∪ 𝐹 ∧ 𝑦 ⊆ ∪ 𝑥 ) ) → ∪ 𝑥 ∈ 𝐹 )
26 6 13 22 24 25 syl13anc ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) ) → ∪ 𝑥 ∈ 𝐹 )
27 elun1 ⊢ ( ∪ 𝑥 ∈ 𝐹 → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) )
28 26 27 syl ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) ∧ ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) ) → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) )
29 28 ex ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) → ( ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) )
30 29 exlimdv ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) → ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ¬ 𝑦 ∈ { ∅ } ) → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) )
31 5 30 syl5bi ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) → ( ¬ 𝑥 ⊆ { ∅ } → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) )
32 uni0b ⊢ ( ∪ 𝑥 = ∅ ↔ 𝑥 ⊆ { ∅ } )
33 ssun2 ⊢ { ∅ } ⊆ ( 𝐹 ∪ { ∅ } )
34 17 snid ⊢ ∅ ∈ { ∅ }
35 33 34 sselii ⊢ ∅ ∈ ( 𝐹 ∪ { ∅ } )
36 eleq1 ⊢ ( ∪ 𝑥 = ∅ → ( ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ↔ ∅ ∈ ( 𝐹 ∪ { ∅ } ) ) )
37 35 36 mpbiri ⊢ ( ∪ 𝑥 = ∅ → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) )
38 32 37 sylbir ⊢ ( 𝑥 ⊆ { ∅ } → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) )
39 31 38 pm2.61d2 ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) ) → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) )
40 39 ex ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) )
41 40 alrimiv ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ∀ 𝑥 ( 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) )
42 filin ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 )
43 elun1 ⊢ ( ( 𝑥 ∩ 𝑦 ) ∈ 𝐹 → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
44 42 43 syl ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
45 44 3expa ⊢ ( ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) ∧ 𝑦 ∈ 𝐹 ) → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
46 45 ralrimiva ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
47 elsni ⊢ ( 𝑦 ∈ { ∅ } → 𝑦 = ∅ )
48 ineq2 ⊢ ( 𝑦 = ∅ → ( 𝑥 ∩ 𝑦 ) = ( 𝑥 ∩ ∅ ) )
49 in0 ⊢ ( 𝑥 ∩ ∅ ) = ∅
50 48 49 eqtrdi ⊢ ( 𝑦 = ∅ → ( 𝑥 ∩ 𝑦 ) = ∅ )
51 50 35 eqeltrdi ⊢ ( 𝑦 = ∅ → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
52 47 51 syl ⊢ ( 𝑦 ∈ { ∅ } → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
53 52 rgen ⊢ ∀ 𝑦 ∈ { ∅ } ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } )
54 ralun ⊢ ( ( ∀ 𝑦 ∈ 𝐹 ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) ∧ ∀ 𝑦 ∈ { ∅ } ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) ) → ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
55 46 53 54 sylancl ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
56 55 ralrimiva ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
57 elsni ⊢ ( 𝑥 ∈ { ∅ } → 𝑥 = ∅ )
58 ineq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∩ 𝑦 ) = ( ∅ ∩ 𝑦 ) )
59 0in ⊢ ( ∅ ∩ 𝑦 ) = ∅
60 58 59 eqtrdi ⊢ ( 𝑥 = ∅ → ( 𝑥 ∩ 𝑦 ) = ∅ )
61 60 35 eqeltrdi ⊢ ( 𝑥 = ∅ → ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
62 61 ralrimivw ⊢ ( 𝑥 = ∅ → ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
63 57 62 syl ⊢ ( 𝑥 ∈ { ∅ } → ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
64 63 rgen ⊢ ∀ 𝑥 ∈ { ∅ } ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } )
65 ralun ⊢ ( ( ∀ 𝑥 ∈ 𝐹 ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) ∧ ∀ 𝑥 ∈ { ∅ } ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) ) → ∀ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
66 56 64 65 sylancl ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ∀ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) )
67 p0ex ⊢ { ∅ } ∈ V
68 unexg ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ { ∅ } ∈ V ) → ( 𝐹 ∪ { ∅ } ) ∈ V )
69 67 68 mpan2 ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( 𝐹 ∪ { ∅ } ) ∈ V )
70 istopg ⊢ ( ( 𝐹 ∪ { ∅ } ) ∈ V → ( ( 𝐹 ∪ { ∅ } ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) ∧ ∀ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) ) ) )
71 69 70 syl ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( ( 𝐹 ∪ { ∅ } ) ∈ Top ↔ ( ∀ 𝑥 ( 𝑥 ⊆ ( 𝐹 ∪ { ∅ } ) → ∪ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) ∧ ∀ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ∀ 𝑦 ∈ ( 𝐹 ∪ { ∅ } ) ( 𝑥 ∩ 𝑦 ) ∈ ( 𝐹 ∪ { ∅ } ) ) ) )
72 41 66 71 mpbir2and ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( 𝐹 ∪ { ∅ } ) ∈ Top )
73 21 cldopn ⊢ ( 𝑥 ∈ ( Clsd ‘ ( 𝐹 ∪ { ∅ } ) ) → ( ∪ 𝐹 ∖ 𝑥 ) ∈ ( 𝐹 ∪ { ∅ } ) )
74 elun ⊢ ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ ( 𝐹 ∪ { ∅ } ) ↔ ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 ∨ ( ∪ 𝐹 ∖ 𝑥 ) ∈ { ∅ } ) )
75 73 74 sylib ⊢ ( 𝑥 ∈ ( Clsd ‘ ( 𝐹 ∪ { ∅ } ) ) → ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 ∨ ( ∪ 𝐹 ∖ 𝑥 ) ∈ { ∅ } ) )
76 elun ⊢ ( 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ↔ ( 𝑥 ∈ 𝐹 ∨ 𝑥 ∈ { ∅ } ) )
77 filfbas ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → 𝐹 ∈ ( fBas ‘ ∪ 𝐹 ) )
78 fbncp ⊢ ( ( 𝐹 ∈ ( fBas ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ¬ ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 )
79 77 78 sylan ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ¬ ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 )
80 79 pm2.21d ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ 𝐹 ) → ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 → 𝑥 = ∅ ) )
81 80 ex ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( 𝑥 ∈ 𝐹 → ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 → 𝑥 = ∅ ) ) )
82 57 a1i13 ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( 𝑥 ∈ { ∅ } → ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 → 𝑥 = ∅ ) ) )
83 81 82 jaod ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( ( 𝑥 ∈ 𝐹 ∨ 𝑥 ∈ { ∅ } ) → ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 → 𝑥 = ∅ ) ) )
84 76 83 syl5bi ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) → ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 → 𝑥 = ∅ ) ) )
85 84 imp ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) → ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 → 𝑥 = ∅ ) )
86 elsni ⊢ ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ { ∅ } → ( ∪ 𝐹 ∖ 𝑥 ) = ∅ )
87 elssuni ⊢ ( 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) → 𝑥 ⊆ ∪ ( 𝐹 ∪ { ∅ } ) )
88 87 21 sseqtrrdi ⊢ ( 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) → 𝑥 ⊆ ∪ 𝐹 )
89 88 adantl ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) → 𝑥 ⊆ ∪ 𝐹 )
90 ssdif0 ⊢ ( ∪ 𝐹 ⊆ 𝑥 ↔ ( ∪ 𝐹 ∖ 𝑥 ) = ∅ )
91 90 biimpri ⊢ ( ( ∪ 𝐹 ∖ 𝑥 ) = ∅ → ∪ 𝐹 ⊆ 𝑥 )
92 eqss ⊢ ( 𝑥 = ∪ 𝐹 ↔ ( 𝑥 ⊆ ∪ 𝐹 ∧ ∪ 𝐹 ⊆ 𝑥 ) )
93 92 simplbi2 ⊢ ( 𝑥 ⊆ ∪ 𝐹 → ( ∪ 𝐹 ⊆ 𝑥 → 𝑥 = ∪ 𝐹 ) )
94 89 91 93 syl2im ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) → ( ( ∪ 𝐹 ∖ 𝑥 ) = ∅ → 𝑥 = ∪ 𝐹 ) )
95 86 94 syl5 ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) → ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ { ∅ } → 𝑥 = ∪ 𝐹 ) )
96 85 95 orim12d ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) → ( ( ( ∪ 𝐹 ∖ 𝑥 ) ∈ 𝐹 ∨ ( ∪ 𝐹 ∖ 𝑥 ) ∈ { ∅ } ) → ( 𝑥 = ∅ ∨ 𝑥 = ∪ 𝐹 ) ) )
97 75 96 syl5 ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) ∧ 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ) → ( 𝑥 ∈ ( Clsd ‘ ( 𝐹 ∪ { ∅ } ) ) → ( 𝑥 = ∅ ∨ 𝑥 = ∪ 𝐹 ) ) )
98 97 expimpd ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( ( 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ∧ 𝑥 ∈ ( Clsd ‘ ( 𝐹 ∪ { ∅ } ) ) ) → ( 𝑥 = ∅ ∨ 𝑥 = ∪ 𝐹 ) ) )
99 elin ⊢ ( 𝑥 ∈ ( ( 𝐹 ∪ { ∅ } ) ∩ ( Clsd ‘ ( 𝐹 ∪ { ∅ } ) ) ) ↔ ( 𝑥 ∈ ( 𝐹 ∪ { ∅ } ) ∧ 𝑥 ∈ ( Clsd ‘ ( 𝐹 ∪ { ∅ } ) ) ) )
100 vex ⊢ 𝑥 ∈ V
101 100 elpr ⊢ ( 𝑥 ∈ { ∅ , ∪ 𝐹 } ↔ ( 𝑥 = ∅ ∨ 𝑥 = ∪ 𝐹 ) )
102 98 99 101 3imtr4g ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( 𝑥 ∈ ( ( 𝐹 ∪ { ∅ } ) ∩ ( Clsd ‘ ( 𝐹 ∪ { ∅ } ) ) ) → 𝑥 ∈ { ∅ , ∪ 𝐹 } ) )
103 102 ssrdv ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( ( 𝐹 ∪ { ∅ } ) ∩ ( Clsd ‘ ( 𝐹 ∪ { ∅ } ) ) ) ⊆ { ∅ , ∪ 𝐹 } )
104 21 isconn2 ⊢ ( ( 𝐹 ∪ { ∅ } ) ∈ Conn ↔ ( ( 𝐹 ∪ { ∅ } ) ∈ Top ∧ ( ( 𝐹 ∪ { ∅ } ) ∩ ( Clsd ‘ ( 𝐹 ∪ { ∅ } ) ) ) ⊆ { ∅ , ∪ 𝐹 } ) )
105 72 103 104 sylanbrc ⊢ ( 𝐹 ∈ ( Fil ‘ ∪ 𝐹 ) → ( 𝐹 ∪ { ∅ } ) ∈ Conn )
106 4 105 syl ⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → ( 𝐹 ∪ { ∅ } ) ∈ Conn )