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 φ D ∞Met X
metelcls.5 φ S X
Assertion metelcls φ P cls J S f f : S f t J P


Step Hyp Ref Expression
1 metelcls.2 J = MetOpen D
2 metelcls.3 φ D ∞Met X
3 metelcls.5 φ S X
4 1 met1stc D ∞Met X J 1 st 𝜔
5 2 4 syl φ J 1 st 𝜔
6 1 mopnuni D ∞Met X X = J
7 2 6 syl φ X = J
8 3 7 sseqtrd φ S J
9 eqid J = J
10 9 1stcelcls J 1 st 𝜔 S J P cls J S f f : S f t J P
11 5 8 10 syl2anc φ P cls J S f f : S f t J P