Metamath Proof Explorer

Theorem metcld

Description: A subset of a metric space is closed iff every convergent sequence on it converges to a point in the subset. Theorem 1.4-6(b) of Kreyszig p. 30. (Contributed by NM, 11-Nov-2007) (Revised by Mario Carneiro, 1-May-2014)

Ref Expression
Hypothesis metcld.2 ⊢ J = MetOpen ⁡ D
Assertion metcld ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → S ∈ Clsd ⁡ J ↔ ∀ x ∀ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J x → x ∈ S

Proof

Step Hyp Ref Expression
1 metcld.2 ⊢ J = MetOpen ⁡ D
2 1 mopntop ⊢ D ∈ ∞Met ⁡ X → J ∈ Top
3 1 mopnuni ⊢ D ∈ ∞Met ⁡ X → X = ⋃ J
4 3 sseq2d ⊢ D ∈ ∞Met ⁡ X → S ⊆ X ↔ S ⊆ ⋃ J
5 4 biimpa ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → S ⊆ ⋃ J
6 eqid ⊢ ⋃ J = ⋃ J
7 6 iscld4 ⊢ J ∈ Top ∧ S ⊆ ⋃ J → S ∈ Clsd ⁡ J ↔ cls ⁡ J ⁡ S ⊆ S
8 2 5 7 syl2an2r ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → S ∈ Clsd ⁡ J ↔ cls ⁡ J ⁡ S ⊆ S
9 19.23v ⊢ ∀ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J x → x ∈ S ↔ ∃ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J x → x ∈ S
10 simpl ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → D ∈ ∞Met ⁡ X
11 simpr ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → S ⊆ X
12 1 10 11 metelcls ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → x ∈ cls ⁡ J ⁡ S ↔ ∃ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J x
13 12 imbi1d ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → x ∈ cls ⁡ J ⁡ S → x ∈ S ↔ ∃ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J x → x ∈ S
14 9 13 bitr4id ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → ∀ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J x → x ∈ S ↔ x ∈ cls ⁡ J ⁡ S → x ∈ S
15 14 albidv ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → ∀ x ∀ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J x → x ∈ S ↔ ∀ x x ∈ cls ⁡ J ⁡ S → x ∈ S
16 df-ss ⊢ cls ⁡ J ⁡ S ⊆ S ↔ ∀ x x ∈ cls ⁡ J ⁡ S → x ∈ S
17 15 16 bitr4di ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → ∀ x ∀ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J x → x ∈ S ↔ cls ⁡ J ⁡ S ⊆ S
18 8 17 bitr4d ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → S ∈ Clsd ⁡ J ↔ ∀ x ∀ f f : ℕ ⟶ S ∧ f ⇝t ⁡ J x → x ∈ S