Metamath Proof Explorer

Theorem flimopn

Description: The condition for being a limit point of a filter still holds if one only considers open neighborhoods. (Contributed by Jeff Hankins, 4-Sep-2009) (Proof shortened by Mario Carneiro, 9-Apr-2015)

Ref Expression
Assertion flimopn 
|- ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. x e. J ( A e. x -> x e. F ) ) ) )

Proof

Step Hyp Ref Expression
1 elflim 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) ) )
2 dfss3 
 |-  ( ( ( nei ` J ) ` { A } ) C_ F <-> A. y e. ( ( nei ` J ) ` { A } ) y e. F )
3 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
4 3 ad2antrr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) -> J e. Top )
5 opnneip 
 |-  ( ( J e. Top /\ x e. J /\ A e. x ) -> x e. ( ( nei ` J ) ` { A } ) )
6 5 3expb 
 |-  ( ( J e. Top /\ ( x e. J /\ A e. x ) ) -> x e. ( ( nei ` J ) ` { A } ) )
7 4 6 sylan 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( x e. J /\ A e. x ) ) -> x e. ( ( nei ` J ) ` { A } ) )
8 eleq1 
 |-  ( y = x -> ( y e. F <-> x e. F ) )
9 8 rspcv 
 |-  ( x e. ( ( nei ` J ) ` { A } ) -> ( A. y e. ( ( nei ` J ) ` { A } ) y e. F -> x e. F ) )
10 7 9 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ ( x e. J /\ A e. x ) ) -> ( A. y e. ( ( nei ` J ) ` { A } ) y e. F -> x e. F ) )
11 10 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ x e. J ) -> ( A e. x -> ( A. y e. ( ( nei ` J ) ` { A } ) y e. F -> x e. F ) ) )
12 11 com23 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ x e. J ) -> ( A. y e. ( ( nei ` J ) ` { A } ) y e. F -> ( A e. x -> x e. F ) ) )
13 12 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) -> ( A. y e. ( ( nei ` J ) ` { A } ) y e. F -> A. x e. J ( A e. x -> x e. F ) ) )
14 simpr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> y e. ( ( nei ` J ) ` { A } ) )
15 3 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> J e. Top )
16 simplr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> A e. X )
17 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
18 17 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> X = U. J )
19 16 18 eleqtrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> A e. U. J )
20 19 snssd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> { A } C_ U. J )
21 eqid 
 |-  U. J = U. J
22 21 neii1 
 |-  ( ( J e. Top /\ y e. ( ( nei ` J ) ` { A } ) ) -> y C_ U. J )
23 4 22 sylan 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> y C_ U. J )
24 21 neiint 
 |-  ( ( J e. Top /\ { A } C_ U. J /\ y C_ U. J ) -> ( y e. ( ( nei ` J ) ` { A } ) <-> { A } C_ ( ( int ` J ) ` y ) ) )
25 15 20 23 24 syl3anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( y e. ( ( nei ` J ) ` { A } ) <-> { A } C_ ( ( int ` J ) ` y ) ) )
26 14 25 mpbid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> { A } C_ ( ( int ` J ) ` y ) )
27 snssg 
 |-  ( A e. X -> ( A e. ( ( int ` J ) ` y ) <-> { A } C_ ( ( int ` J ) ` y ) ) )
28 27 ad2antlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( A e. ( ( int ` J ) ` y ) <-> { A } C_ ( ( int ` J ) ` y ) ) )
29 26 28 mpbird 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> A e. ( ( int ` J ) ` y ) )
30 21 ntropn 
 |-  ( ( J e. Top /\ y C_ U. J ) -> ( ( int ` J ) ` y ) e. J )
31 15 23 30 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( ( int ` J ) ` y ) e. J )
32 eleq2 
 |-  ( x = ( ( int ` J ) ` y ) -> ( A e. x <-> A e. ( ( int ` J ) ` y ) ) )
33 eleq1 
 |-  ( x = ( ( int ` J ) ` y ) -> ( x e. F <-> ( ( int ` J ) ` y ) e. F ) )
34 32 33 imbi12d 
 |-  ( x = ( ( int ` J ) ` y ) -> ( ( A e. x -> x e. F ) <-> ( A e. ( ( int ` J ) ` y ) -> ( ( int ` J ) ` y ) e. F ) ) )
35 34 rspcv 
 |-  ( ( ( int ` J ) ` y ) e. J -> ( A. x e. J ( A e. x -> x e. F ) -> ( A e. ( ( int ` J ) ` y ) -> ( ( int ` J ) ` y ) e. F ) ) )
36 31 35 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( A. x e. J ( A e. x -> x e. F ) -> ( A e. ( ( int ` J ) ` y ) -> ( ( int ` J ) ` y ) e. F ) ) )
37 29 36 mpid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( A. x e. J ( A e. x -> x e. F ) -> ( ( int ` J ) ` y ) e. F ) )
38 simpllr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> F e. ( Fil ` X ) )
39 21 ntrss2 
 |-  ( ( J e. Top /\ y C_ U. J ) -> ( ( int ` J ) ` y ) C_ y )
40 15 23 39 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( ( int ` J ) ` y ) C_ y )
41 23 18 sseqtrrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> y C_ X )
42 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( ( ( int ` J ) ` y ) e. F /\ y C_ X /\ ( ( int ` J ) ` y ) C_ y ) ) -> y e. F )
43 42 3exp2 
 |-  ( F e. ( Fil ` X ) -> ( ( ( int ` J ) ` y ) e. F -> ( y C_ X -> ( ( ( int ` J ) ` y ) C_ y -> y e. F ) ) ) )
44 43 com24 
 |-  ( F e. ( Fil ` X ) -> ( ( ( int ` J ) ` y ) C_ y -> ( y C_ X -> ( ( ( int ` J ) ` y ) e. F -> y e. F ) ) ) )
45 38 40 41 44 syl3c 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( ( ( int ` J ) ` y ) e. F -> y e. F ) )
46 37 45 syld 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) /\ y e. ( ( nei ` J ) ` { A } ) ) -> ( A. x e. J ( A e. x -> x e. F ) -> y e. F ) )
47 46 ralrimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) -> ( A. x e. J ( A e. x -> x e. F ) -> A. y e. ( ( nei ` J ) ` { A } ) y e. F ) )
48 13 47 impbid 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) -> ( A. y e. ( ( nei ` J ) ` { A } ) y e. F <-> A. x e. J ( A e. x -> x e. F ) ) )
49 2 48 syl5bb 
 |-  ( ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) /\ A e. X ) -> ( ( ( nei ` J ) ` { A } ) C_ F <-> A. x e. J ( A e. x -> x e. F ) ) )
50 49 pm5.32da 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( ( A e. X /\ ( ( nei ` J ) ` { A } ) C_ F ) <-> ( A e. X /\ A. x e. J ( A e. x -> x e. F ) ) ) )
51 1 50 bitrd 
 |-  ( ( J e. ( TopOn ` X ) /\ F e. ( Fil ` X ) ) -> ( A e. ( J fLim F ) <-> ( A e. X /\ A. x e. J ( A e. x -> x e. F ) ) ) )