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

Metamath Proof Explorer

Theorem lmcls

Description: Any convergent sequence of points in a subset of a topological space converges to a point in the closure of the subset. (Contributed by Mario Carneiro, 30-Dec-2013) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypotheses lmff.1 
|- Z = ( ZZ>= ` M )
lmff.3 
|- ( ph -> J e. ( TopOn ` X ) )
lmff.4 
|- ( ph -> M e. ZZ )
lmcls.5 
|- ( ph -> F ( ~~>t ` J ) P )
lmcls.7 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. S )
lmcls.8 
|- ( ph -> S C_ X )
Assertion lmcls 
|- ( ph -> P e. ( ( cls ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 lmff.1 
 |-  Z = ( ZZ>= ` M )
2 lmff.3 
 |-  ( ph -> J e. ( TopOn ` X ) )
3 lmff.4 
 |-  ( ph -> M e. ZZ )
4 lmcls.5 
 |-  ( ph -> F ( ~~>t ` J ) P )
5 lmcls.7 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. S )
6 lmcls.8 
 |-  ( ph -> S C_ X )
7 2 1 3 lmbr2 
 |-  ( ph -> ( F ( ~~>t ` J ) P <-> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
8 4 7 mpbid 
 |-  ( ph -> ( F e. ( X ^pm CC ) /\ P e. X /\ A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
9 8 simp3d 
 |-  ( ph -> A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
10 1 r19.2uz 
 |-  ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) -> E. k e. Z ( k e. dom F /\ ( F ` k ) e. u ) )
11 inelcm 
 |-  ( ( ( F ` k ) e. u /\ ( F ` k ) e. S ) -> ( u i^i S ) =/= (/) )
12 11 a1i 
 |-  ( ( ph /\ k e. Z ) -> ( ( ( F ` k ) e. u /\ ( F ` k ) e. S ) -> ( u i^i S ) =/= (/) ) )
13 5 12 mpan2d 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) e. u -> ( u i^i S ) =/= (/) ) )
14 13 adantld 
 |-  ( ( ph /\ k e. Z ) -> ( ( k e. dom F /\ ( F ` k ) e. u ) -> ( u i^i S ) =/= (/) ) )
15 14 rexlimdva 
 |-  ( ph -> ( E. k e. Z ( k e. dom F /\ ( F ` k ) e. u ) -> ( u i^i S ) =/= (/) ) )
16 10 15 syl5 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) -> ( u i^i S ) =/= (/) ) )
17 16 imim2d 
 |-  ( ph -> ( ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) -> ( P e. u -> ( u i^i S ) =/= (/) ) ) )
18 17 ralimdv 
 |-  ( ph -> ( A. u e. J ( P e. u -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) -> A. u e. J ( P e. u -> ( u i^i S ) =/= (/) ) ) )
19 9 18 mpd 
 |-  ( ph -> A. u e. J ( P e. u -> ( u i^i S ) =/= (/) ) )
20 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
21 2 20 syl 
 |-  ( ph -> J e. Top )
22 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
23 2 22 syl 
 |-  ( ph -> X = U. J )
24 6 23 sseqtrd 
 |-  ( ph -> S C_ U. J )
25 lmcl 
 |-  ( ( J e. ( TopOn ` X ) /\ F ( ~~>t ` J ) P ) -> P e. X )
26 2 4 25 syl2anc 
 |-  ( ph -> P e. X )
27 26 23 eleqtrd 
 |-  ( ph -> P e. U. J )
28 eqid 
 |-  U. J = U. J
29 28 elcls 
 |-  ( ( J e. Top /\ S C_ U. J /\ P e. U. J ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. u e. J ( P e. u -> ( u i^i S ) =/= (/) ) ) )
30 21 24 27 29 syl3anc 
 |-  ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> A. u e. J ( P e. u -> ( u i^i S ) =/= (/) ) ) )
31 19 30 mpbird 
 |-  ( ph -> P e. ( ( cls ` J ) ` S ) )