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 syl5bb ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → ( ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) → 𝑥𝑆 ) ↔ ( 𝑥 ∈ ( ( ⇝𝑡𝐽 ) “ ( 𝑆m ℕ ) ) → 𝑥𝑆 ) ) )
18 17 albidv ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → ( ∀ 𝑥𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) → 𝑥𝑆 ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( ⇝𝑡𝐽 ) “ ( 𝑆m ℕ ) ) → 𝑥𝑆 ) ) )
19 dfss2 ( ( ( ⇝𝑡𝐽 ) “ ( 𝑆m ℕ ) ) ⊆ 𝑆 ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( ⇝𝑡𝐽 ) “ ( 𝑆m ℕ ) ) → 𝑥𝑆 ) )
20 18 19 bitr4di ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → ( ∀ 𝑥𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆𝑓 ( ⇝𝑡𝐽 ) 𝑥 ) → 𝑥𝑆 ) ↔ ( ( ⇝𝑡𝐽 ) “ ( 𝑆m ℕ ) ) ⊆ 𝑆 ) )
21 2 20 bitrd ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) → ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) ↔ ( ( ⇝𝑡𝐽 ) “ ( 𝑆m ℕ ) ) ⊆ 𝑆 ) )