Metamath Proof Explorer

Theorem hausflimlem

Description: If A and B are both limits of the same filter, then all neighborhoods of A and B intersect. (Contributed by Mario Carneiro, 21-Sep-2015)

Ref Expression
Assertion hausflimlem ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → U ∩ V ≠ ∅

Proof

Step Hyp Ref Expression
1 simp1l ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → A ∈ J fLim F
2 eqid ⊢ ⋃ J = ⋃ J
3 2 flimfil ⊢ A ∈ J fLim F → F ∈ Fil ⁡ ⋃ J
4 1 3 syl ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → F ∈ Fil ⁡ ⋃ J
5 flimtop ⊢ A ∈ J fLim F → J ∈ Top
6 1 5 syl ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → J ∈ Top
7 simp2l ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → U ∈ J
8 simp3l ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → A ∈ U
9 opnneip ⊢ J ∈ Top ∧ U ∈ J ∧ A ∈ U → U ∈ nei ⁡ J ⁡ A
10 6 7 8 9 syl3anc ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → U ∈ nei ⁡ J ⁡ A
11 flimnei ⊢ A ∈ J fLim F ∧ U ∈ nei ⁡ J ⁡ A → U ∈ F
12 1 10 11 syl2anc ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → U ∈ F
13 simp1r ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → B ∈ J fLim F
14 simp2r ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → V ∈ J
15 simp3r ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → B ∈ V
16 opnneip ⊢ J ∈ Top ∧ V ∈ J ∧ B ∈ V → V ∈ nei ⁡ J ⁡ B
17 6 14 15 16 syl3anc ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → V ∈ nei ⁡ J ⁡ B
18 flimnei ⊢ B ∈ J fLim F ∧ V ∈ nei ⁡ J ⁡ B → V ∈ F
19 13 17 18 syl2anc ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → V ∈ F
20 filinn0 ⊢ F ∈ Fil ⁡ ⋃ J ∧ U ∈ F ∧ V ∈ F → U ∩ V ≠ ∅
21 4 12 19 20 syl3anc ⊢ A ∈ J fLim F ∧ B ∈ J fLim F ∧ U ∈ J ∧ V ∈ J ∧ A ∈ U ∧ B ∈ V → U ∩ V ≠ ∅