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 ⊢ φ → D ∈ ∞Met ⁡ X
metelcls.5 ⊢ φ → S ⊆ X
Assertion metelcls ⊢ φ → P ∈ cls ⁡ J ⁡ S ↔ ∃ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J P

Proof

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