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

Metamath Proof Explorer

Theorem lmcld

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

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 )
lmcld.8 
|- ( ph -> S e. ( Clsd ` J ) )
Assertion lmcld 
|- ( ph -> P e. 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 lmcld.8 
 |-  ( ph -> S e. ( Clsd ` J ) )
7 eqid 
 |-  U. J = U. J
8 7 cldss 
 |-  ( S e. ( Clsd ` J ) -> S C_ U. J )
9 6 8 syl 
 |-  ( ph -> S C_ U. J )
10 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
11 2 10 syl 
 |-  ( ph -> X = U. J )
12 9 11 sseqtrrd 
 |-  ( ph -> S C_ X )
13 1 2 3 4 5 12 lmcls 
 |-  ( ph -> P e. ( ( cls ` J ) ` S ) )
14 cldcls 
 |-  ( S e. ( Clsd ` J ) -> ( ( cls ` J ) ` S ) = S )
15 6 14 syl 
 |-  ( ph -> ( ( cls ` J ) ` S ) = S )
16 13 15 eleqtrd 
 |-  ( ph -> P e. S )