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 = ( MetOpen ` D )
Assertion metcld2 
|- ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( ~~>t ` J ) " ( S ^m NN ) ) C_ S ) )

Proof

Step Hyp Ref Expression
1 metcld.2 
 |-  J = ( MetOpen ` D )
2 1 metcld 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> A. x A. f ( ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) ) )
3 19.23v 
 |-  ( A. f ( ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) <-> ( E. f ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) )
4 vex 
 |-  x e. _V
5 4 elima2 
 |-  ( x e. ( ( ~~>t ` J ) " ( S ^m NN ) ) <-> E. f ( f e. ( S ^m NN ) /\ f ( ~~>t ` J ) x ) )
6 id 
 |-  ( S C_ X -> S C_ X )
7 elfvdm 
 |-  ( D e. ( *Met ` X ) -> X e. dom *Met )
8 ssexg 
 |-  ( ( S C_ X /\ X e. dom *Met ) -> S e. _V )
9 6 7 8 syl2anr 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> S e. _V )
10 nnex 
 |-  NN e. _V
11 elmapg 
 |-  ( ( S e. _V /\ NN e. _V ) -> ( f e. ( S ^m NN ) <-> f : NN --> S ) )
12 9 10 11 sylancl 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( f e. ( S ^m NN ) <-> f : NN --> S ) )
13 12 anbi1d 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( ( f e. ( S ^m NN ) /\ f ( ~~>t ` J ) x ) <-> ( f : NN --> S /\ f ( ~~>t ` J ) x ) ) )
14 13 exbidv 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( E. f ( f e. ( S ^m NN ) /\ f ( ~~>t ` J ) x ) <-> E. f ( f : NN --> S /\ f ( ~~>t ` J ) x ) ) )
15 5 14 bitr2id 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( E. f ( f : NN --> S /\ f ( ~~>t ` J ) x ) <-> x e. ( ( ~~>t ` J ) " ( S ^m NN ) ) ) )
16 15 imbi1d 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( ( E. f ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) <-> ( x e. ( ( ~~>t ` J ) " ( S ^m NN ) ) -> x e. S ) ) )
17 3 16 syl5bb 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( A. f ( ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) <-> ( x e. ( ( ~~>t ` J ) " ( S ^m NN ) ) -> x e. S ) ) )
18 17 albidv 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( A. x A. f ( ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) <-> A. x ( x e. ( ( ~~>t ` J ) " ( S ^m NN ) ) -> x e. S ) ) )
19 dfss2 
 |-  ( ( ( ~~>t ` J ) " ( S ^m NN ) ) C_ S <-> A. x ( x e. ( ( ~~>t ` J ) " ( S ^m NN ) ) -> x e. S ) )
20 18 19 bitr4di 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( A. x A. f ( ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) <-> ( ( ~~>t ` J ) " ( S ^m NN ) ) C_ S ) )
21 2 20 bitrd 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( ~~>t ` J ) " ( S ^m NN ) ) C_ S ) )