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 β„• ) ) βŠ† 𝑆 ) )