Theorem metelcls

Description: A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of Kreyszig p. 30. This proof uses countable choice ax-cc . The statement can be generalized to first-countable spaces, not just metrizable spaces. (Contributed by NM, 8-Nov-2007) (Proof shortened by Mario Carneiro, 1-May-2015)

	Ref	Expression
Hypotheses	metelcls.2	|- J = ( MetOpen ` D )
	metelcls.3	|- ( ph -> D e. ( *Met ` X ) )
	metelcls.5	|- ( ph -> S C_ X )
Assertion	metelcls	|- ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )

Proof

Step	Hyp	Ref	Expression
1		metelcls.2	|- J = ( MetOpen ` D )
2		metelcls.3	|- ( ph -> D e. ( *Met ` X ) )
3		metelcls.5	|- ( ph -> S C_ X )
4	1	met1stc	|- ( D e. ( *Met ` X ) -> J e. 1stc )
5	2 4	syl	|- ( ph -> J e. 1stc )
6	1	mopnuni	|- ( D e. ( *Met ` X ) -> X = U. J )
7	2 6	syl	|- ( ph -> X = U. J )
8	3 7	sseqtrd	|- ( ph -> S C_ U. J )
9		eqid	|- U. J = U. J
10	9	1stcelcls	|- ( ( J e. 1stc /\ S C_ U. J ) -> ( P e. ( ( cls ` J ) ` S ) <-> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )
11	5 8 10	syl2anc	|- ( ph -> ( P e. ( ( cls ` J ) ` S ) <-> E. f ( f : NN --> S /\ f ( ~~>t ` J ) P ) ) )