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 ⊢ 𝐽 = ( 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 ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ) ) )