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 J=MetOpenD
Assertion metcld2 D∞MetXSXSClsdJtJSS

Proof

Step Hyp Ref Expression
1 metcld.2 J=MetOpenD
2 1 metcld D∞MetXSXSClsdJxff:SftJxxS
3 19.23v ff:SftJxxSff:SftJxxS
4 vex xV
5 4 elima2 xtJSffSftJx
6 id SXSX
7 elfvdm D∞MetXXdom∞Met
8 ssexg SXXdom∞MetSV
9 6 7 8 syl2anr D∞MetXSXSV
10 nnex V
11 elmapg SVVfSf:S
12 9 10 11 sylancl D∞MetXSXfSf:S
13 12 anbi1d D∞MetXSXfSftJxf:SftJx
14 13 exbidv D∞MetXSXffSftJxff:SftJx
15 5 14 bitr2id D∞MetXSXff:SftJxxtJS
16 15 imbi1d D∞MetXSXff:SftJxxSxtJSxS
17 3 16 bitrid D∞MetXSXff:SftJxxSxtJSxS
18 17 albidv D∞MetXSXxff:SftJxxSxxtJSxS
19 dfss2 tJSSxxtJSxS
20 18 19 bitr4di D∞MetXSXxff:SftJxxStJSS
21 2 20 bitrd D∞MetXSXSClsdJtJSS