# 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}=\mathrm{MetOpen}\left({D}\right)$
metelcls.3 ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
metelcls.5 ${⊢}{\phi }\to {S}\subseteq {X}$
Assertion metelcls

### Proof

Step Hyp Ref Expression
1 metelcls.2 ${⊢}{J}=\mathrm{MetOpen}\left({D}\right)$
2 metelcls.3 ${⊢}{\phi }\to {D}\in \mathrm{\infty Met}\left({X}\right)$
3 metelcls.5 ${⊢}{\phi }\to {S}\subseteq {X}$
4 1 met1stc ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {J}\in {1}^{st}𝜔$
5 2 4 syl ${⊢}{\phi }\to {J}\in {1}^{st}𝜔$
6 1 mopnuni ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to {X}=\bigcup {J}$
7 2 6 syl ${⊢}{\phi }\to {X}=\bigcup {J}$
8 3 7 sseqtrd ${⊢}{\phi }\to {S}\subseteq \bigcup {J}$
9 eqid ${⊢}\bigcup {J}=\bigcup {J}$
10 9 1stcelcls
11 5 8 10 syl2anc