# 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 )`