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 
|- J = ( MetOpen ` D )
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 metcld.2 
 |-  J = ( MetOpen ` D )
2 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
3 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
4 3 sseq2d 
 |-  ( D e. ( *Met ` X ) -> ( S C_ X <-> S C_ U. J ) )
5 4 biimpa 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> S C_ U. J )
6 eqid 
 |-  U. J = U. J
7 6 iscld4 
 |-  ( ( J e. Top /\ S C_ U. J ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) C_ S ) )
8 2 5 7 syl2an2r 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( S e. ( Clsd ` J ) <-> ( ( cls ` J ) ` S ) C_ S ) )
9 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 ) )
10 simpl 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> D e. ( *Met ` X ) )
11 simpr 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> S C_ X )
12 1 10 11 metelcls 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( x e. ( ( cls ` J ) ` S ) <-> E. f ( f : NN --> S /\ f ( ~~>t ` J ) x ) ) )
13 12 imbi1d 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( ( x e. ( ( cls ` J ) ` S ) -> x e. S ) <-> ( E. f ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) ) )
14 9 13 bitr4id 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( A. f ( ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) <-> ( x e. ( ( cls ` J ) ` S ) -> x e. S ) ) )
15 14 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. ( ( cls ` J ) ` S ) -> x e. S ) ) )
16 df-ss 
 |-  ( ( ( cls ` J ) ` S ) C_ S <-> A. x ( x e. ( ( cls ` J ) ` S ) -> x e. S ) )
17 15 16 bitr4di 
 |-  ( ( D e. ( *Met ` X ) /\ S C_ X ) -> ( A. x A. f ( ( f : NN --> S /\ f ( ~~>t ` J ) x ) -> x e. S ) <-> ( ( cls ` J ) ` S ) C_ S ) )
18 8 17 bitr4d 
 |-  ( ( 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 ) ) )