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

Metamath Proof Explorer

Theorem metcld2

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 Mario Carneiro, 1-May-2014)

Ref Expression
Hypothesis metcld.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion metcld2 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) ⊆ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 metcld.2 ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
2 1 metcld ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ) )
3 19.23v ⊢ ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ↔ ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) )
4 vex ⊢ 𝑥 ∈ V
5 4 elima2 ⊢ ( 𝑥 ∈ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) ↔ ∃ 𝑓 ( 𝑓 ∈ ( 𝑆 ↑m ℕ ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) )
6 id ⊢ ( 𝑆 ⊆ 𝑋 → 𝑆 ⊆ 𝑋 )
7 elfvdm ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
8 ssexg ⊢ ( ( 𝑆 ⊆ 𝑋 ∧ 𝑋 ∈ dom ∞Met ) → 𝑆 ∈ V )
9 6 7 8 syl2anr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ∈ V )
10 nnex ⊢ ℕ ∈ V
11 elmapg ⊢ ( ( 𝑆 ∈ V ∧ ℕ ∈ V ) → ( 𝑓 ∈ ( 𝑆 ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ 𝑆 ) )
12 9 10 11 sylancl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑓 ∈ ( 𝑆 ↑m ℕ ) ↔ 𝑓 : ℕ ⟶ 𝑆 ) )
13 12 anbi1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝑓 ∈ ( 𝑆 ↑m ℕ ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ↔ ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) )
14 13 exbidv ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∃ 𝑓 ( 𝑓 ∈ ( 𝑆 ↑m ℕ ) ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ↔ ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ) )
15 5 14 bitr2id ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) ↔ 𝑥 ∈ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) ) )
16 15 imbi1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ( ∃ 𝑓 ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ↔ ( 𝑥 ∈ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) → 𝑥 ∈ 𝑆 ) ) )
17 3 16 bitrid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ↔ ( 𝑥 ∈ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) → 𝑥 ∈ 𝑆 ) ) )
18 17 albidv ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) → 𝑥 ∈ 𝑆 ) ) )
19 df-ss ⊢ ( ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) ⊆ 𝑆 ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) → 𝑥 ∈ 𝑆 ) )
20 18 19 bitr4di ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ↔ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) ⊆ 𝑆 ) )
21 2 20 bitrd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( ⇝𝑡 ‘ 𝐽 ) “ ( 𝑆 ↑m ℕ ) ) ⊆ 𝑆 ) )