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 ‘ 𝐽 ) ↔ ∀ 𝑥 ∀ 𝑓 ( ( 𝑓 : ℕ ⟶ 𝑆 ∧ 𝑓 ( ⇝𝑡 ‘ 𝐽 ) 𝑥 ) → 𝑥 ∈ 𝑆 ) ) )