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 )