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 dfss2 ⊒ ( ( ( cls β€˜ 𝐽 ) β€˜ 𝑆 ) βŠ† 𝑆 ↔ βˆ€ π‘₯ ( π‘₯ ∈ ( ( cls β€˜ 𝐽 ) β€˜ 𝑆 ) β†’ π‘₯ ∈ 𝑆 ) )
17 15 16 bitr4di ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ) β†’ ( βˆ€ π‘₯ βˆ€ 𝑓 ( ( 𝑓 : β„• ⟢ 𝑆 ∧ 𝑓 ( ⇝𝑑 β€˜ 𝐽 ) π‘₯ ) β†’ π‘₯ ∈ 𝑆 ) ↔ ( ( cls β€˜ 𝐽 ) β€˜ 𝑆 ) βŠ† 𝑆 ) )
18 8 17 bitr4d ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ) β†’ ( 𝑆 ∈ ( Clsd β€˜ 𝐽 ) ↔ βˆ€ π‘₯ βˆ€ 𝑓 ( ( 𝑓 : β„• ⟢ 𝑆 ∧ 𝑓 ( ⇝𝑑 β€˜ 𝐽 ) π‘₯ ) β†’ π‘₯ ∈ 𝑆 ) ) )