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

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 ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝑈 ∩ 𝑉 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 simp1l ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐴 ∈ ( 𝐽 fLim 𝐹 ) )
2 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
3 2 flimfil ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
4 1 3 syl ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) )
5 flimtop ⊢ ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) → 𝐽 ∈ Top )
6 1 5 syl ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐽 ∈ Top )
7 simp2l ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝑈 ∈ 𝐽 )
8 simp3l ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑈 )
9 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑈 ∈ 𝐽 ∧ 𝐴 ∈ 𝑈 ) → 𝑈 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
10 6 7 8 9 syl3anc ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝑈 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) )
11 flimnei ⊢ ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑈 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐴 } ) ) → 𝑈 ∈ 𝐹 )
12 1 10 11 syl2anc ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝑈 ∈ 𝐹 )
13 simp1r ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐵 ∈ ( 𝐽 fLim 𝐹 ) )
14 simp2r ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝑉 ∈ 𝐽 )
15 simp3r ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
16 opnneip ⊢ ( ( 𝐽 ∈ Top ∧ 𝑉 ∈ 𝐽 ∧ 𝐵 ∈ 𝑉 ) → 𝑉 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) )
17 6 14 15 16 syl3anc ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝑉 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) )
18 flimnei ⊢ ( ( 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝑉 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝐵 } ) ) → 𝑉 ∈ 𝐹 )
19 13 17 18 syl2anc ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → 𝑉 ∈ 𝐹 )
20 filinn0 ⊢ ( ( 𝐹 ∈ ( Fil ‘ ∪ 𝐽 ) ∧ 𝑈 ∈ 𝐹 ∧ 𝑉 ∈ 𝐹 ) → ( 𝑈 ∩ 𝑉 ) ≠ ∅ )
21 4 12 19 20 syl3anc ⊢ ( ( ( 𝐴 ∈ ( 𝐽 fLim 𝐹 ) ∧ 𝐵 ∈ ( 𝐽 fLim 𝐹 ) ) ∧ ( 𝑈 ∈ 𝐽 ∧ 𝑉 ∈ 𝐽 ) ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝑈 ∩ 𝑉 ) ≠ ∅ )