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	$$⊢\phi \to \left(P\in \mathrm{cls}\left(J\right)\left(S\right)\leftrightarrow \exists f\left(f:\mathbb{N}⟶S\wedge f\underset{t}{⇝}\left(J\right)P\right)\right)$$

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	$$⊢\left(J\in 1^{st}𝜔\wedge S\subseteq \bigcup J\right)\to \left(P\in \mathrm{cls}\left(J\right)\left(S\right)\leftrightarrow \exists f\left(f:\mathbb{N}⟶S\wedge f\underset{t}{⇝}\left(J\right)P\right)\right)$$
11	5 8 10	syl2anc	$$⊢\phi \to \left(P\in \mathrm{cls}\left(J\right)\left(S\right)\leftrightarrow \exists f\left(f:\mathbb{N}⟶S\wedge f\underset{t}{⇝}\left(J\right)P\right)\right)$$