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 
|- ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> ( U i^i V ) =/= (/) )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> A e. ( J fLim F ) )
2 eqid 
 |-  U. J = U. J
3 2 flimfil 
 |-  ( A e. ( J fLim F ) -> F e. ( Fil ` U. J ) )
4 1 3 syl 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> F e. ( Fil ` U. J ) )
5 flimtop 
 |-  ( A e. ( J fLim F ) -> J e. Top )
6 1 5 syl 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> J e. Top )
7 simp2l 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> U e. J )
8 simp3l 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> A e. U )
9 opnneip 
 |-  ( ( J e. Top /\ U e. J /\ A e. U ) -> U e. ( ( nei ` J ) ` { A } ) )
10 6 7 8 9 syl3anc 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> U e. ( ( nei ` J ) ` { A } ) )
11 flimnei 
 |-  ( ( A e. ( J fLim F ) /\ U e. ( ( nei ` J ) ` { A } ) ) -> U e. F )
12 1 10 11 syl2anc 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> U e. F )
13 simp1r 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> B e. ( J fLim F ) )
14 simp2r 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> V e. J )
15 simp3r 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> B e. V )
16 opnneip 
 |-  ( ( J e. Top /\ V e. J /\ B e. V ) -> V e. ( ( nei ` J ) ` { B } ) )
17 6 14 15 16 syl3anc 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> V e. ( ( nei ` J ) ` { B } ) )
18 flimnei 
 |-  ( ( B e. ( J fLim F ) /\ V e. ( ( nei ` J ) ` { B } ) ) -> V e. F )
19 13 17 18 syl2anc 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> V e. F )
20 filinn0 
 |-  ( ( F e. ( Fil ` U. J ) /\ U e. F /\ V e. F ) -> ( U i^i V ) =/= (/) )
21 4 12 19 20 syl3anc 
 |-  ( ( ( A e. ( J fLim F ) /\ B e. ( J fLim F ) ) /\ ( U e. J /\ V e. J ) /\ ( A e. U /\ B e. V ) ) -> ( U i^i V ) =/= (/) )