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

Metamath Proof Explorer

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