This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion metcld ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 metcld.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
3 1 mopnuni ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
4 3 sseq2d ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑆 ⊆ 𝑋 ↔ 𝑆 ⊆ ∪ 𝐽 ) )
5 4 biimpa ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ∪ 𝐽 )
6 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
7 6 iscld4 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) )
8 2 5 7 syl2an2r ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) )
9 19.23v ⊢ ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ↔ ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) )
10 simpl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
11 simpr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ 𝑋 )
12 1 10 11 metelcls ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) )
13 12 imbi1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → 𝑥 ∈ 𝑆 ) ↔ ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ) )
14 9 13 bitr4id ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → 𝑥 ∈ 𝑆 ) ) )
15 14 albidv ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → 𝑥 ∈ 𝑆 ) ) )
16 df-ss ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → 𝑥 ∈ 𝑆 ) )
17 15 16 bitr4di ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑆 ) )
18 8 17 bitr4d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ) )