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	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
	metelcls.3	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
	metelcls.5	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
Assertion	metelcls	⊢ ( 𝜑 → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		metelcls.2	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2		metelcls.3	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3		metelcls.5	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
4	1	met1stc	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ 1stω )
5	2 4	syl	⊢ ( 𝜑 → 𝐽 ∈ 1stω )
6	1	mopnuni	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
7	2 6	syl	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
8	3 7	sseqtrd	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
9		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
10	9	1stcelcls	⊢ ( ( 𝐽 ∈ 1stω ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) )
11	5 8 10	syl2anc	⊢ ( 𝜑 → ( 𝑃 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) )