Metamath Proof Explorer

Theorem fclsopni

Description: An open neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Mario Carneiro, 11-Apr-2015) (Revised by Stefan O'Rear, 8-Aug-2015)

Ref Expression
Assertion fclsopni 
|- ( ( A e. ( J fClus F ) /\ ( U e. J /\ A e. U /\ S e. F ) ) -> ( U i^i S ) =/= (/) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. J = U. J
2 1 fclsfil 
 |-  ( A e. ( J fClus F ) -> F e. ( Fil ` U. J ) )
3 fclstopon 
 |-  ( A e. ( J fClus F ) -> ( J e. ( TopOn ` U. J ) <-> F e. ( Fil ` U. J ) ) )
4 2 3 mpbird 
 |-  ( A e. ( J fClus F ) -> J e. ( TopOn ` U. J ) )
5 fclsopn 
 |-  ( ( J e. ( TopOn ` U. J ) /\ F e. ( Fil ` U. J ) ) -> ( A e. ( J fClus F ) <-> ( A e. U. J /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
6 4 2 5 syl2anc 
 |-  ( A e. ( J fClus F ) -> ( A e. ( J fClus F ) <-> ( A e. U. J /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) ) )
7 6 ibi 
 |-  ( A e. ( J fClus F ) -> ( A e. U. J /\ A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) ) )
8 eleq2 
 |-  ( o = U -> ( A e. o <-> A e. U ) )
9 ineq1 
 |-  ( o = U -> ( o i^i s ) = ( U i^i s ) )
10 9 neeq1d 
 |-  ( o = U -> ( ( o i^i s ) =/= (/) <-> ( U i^i s ) =/= (/) ) )
11 10 ralbidv 
 |-  ( o = U -> ( A. s e. F ( o i^i s ) =/= (/) <-> A. s e. F ( U i^i s ) =/= (/) ) )
12 8 11 imbi12d 
 |-  ( o = U -> ( ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) <-> ( A e. U -> A. s e. F ( U i^i s ) =/= (/) ) ) )
13 12 rspccv 
 |-  ( A. o e. J ( A e. o -> A. s e. F ( o i^i s ) =/= (/) ) -> ( U e. J -> ( A e. U -> A. s e. F ( U i^i s ) =/= (/) ) ) )
14 7 13 simpl2im 
 |-  ( A e. ( J fClus F ) -> ( U e. J -> ( A e. U -> A. s e. F ( U i^i s ) =/= (/) ) ) )
15 ineq2 
 |-  ( s = S -> ( U i^i s ) = ( U i^i S ) )
16 15 neeq1d 
 |-  ( s = S -> ( ( U i^i s ) =/= (/) <-> ( U i^i S ) =/= (/) ) )
17 16 rspccv 
 |-  ( A. s e. F ( U i^i s ) =/= (/) -> ( S e. F -> ( U i^i S ) =/= (/) ) )
18 14 17 syl8 
 |-  ( A e. ( J fClus F ) -> ( U e. J -> ( A e. U -> ( S e. F -> ( U i^i S ) =/= (/) ) ) ) )
19 18 3imp2 
 |-  ( ( A e. ( J fClus F ) /\ ( U e. J /\ A e. U /\ S e. F ) ) -> ( U i^i S ) =/= (/) )