Metamath Proof Explorer

Theorem cmetss

Description: A subspace of a complete metric space is complete iff it is closed in the parent space. Theorem 1.4-7 of Kreyszig p. 30. (Contributed by NM, 28-Jan-2008) (Revised by Mario Carneiro, 15-Oct-2015) (Proof shortened by AV, 9-Oct-2022)

Ref Expression
Hypothesis metsscmetcld.j 
|- J = ( MetOpen ` D )
Assertion cmetss 
|- ( D e. ( CMet ` X ) -> ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> Y e. ( Clsd ` J ) ) )

Proof

Step Hyp Ref Expression
1 metsscmetcld.j 
 |-  J = ( MetOpen ` D )
2 cmetmet 
 |-  ( D e. ( CMet ` X ) -> D e. ( Met ` X ) )
3 1 metsscmetcld 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> Y e. ( Clsd ` J ) )
4 2 3 sylan 
 |-  ( ( D e. ( CMet ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> Y e. ( Clsd ` J ) )
5 2 adantr 
 |-  ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) -> D e. ( Met ` X ) )
6 eqid 
 |-  U. J = U. J
7 6 cldss 
 |-  ( Y e. ( Clsd ` J ) -> Y C_ U. J )
8 7 adantl 
 |-  ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) -> Y C_ U. J )
9 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
10 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
11 5 9 10 3syl 
 |-  ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) -> X = U. J )
12 8 11 sseqtrrd 
 |-  ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) -> Y C_ X )
13 metres2 
 |-  ( ( D e. ( Met ` X ) /\ Y C_ X ) -> ( D |` ( Y X. Y ) ) e. ( Met ` Y ) )
14 5 12 13 syl2anc 
 |-  ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) -> ( D |` ( Y X. Y ) ) e. ( Met ` Y ) )
15 2 9 syl 
 |-  ( D e. ( CMet ` X ) -> D e. ( *Met ` X ) )
16 15 ad2antrr 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> D e. ( *Met ` X ) )
17 12 adantr 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> Y C_ X )
18 eqid 
 |-  ( D |` ( Y X. Y ) ) = ( D |` ( Y X. Y ) )
19 eqid 
 |-  ( MetOpen ` ( D |` ( Y X. Y ) ) ) = ( MetOpen ` ( D |` ( Y X. Y ) ) )
20 18 1 19 metrest 
 |-  ( ( D e. ( *Met ` X ) /\ Y C_ X ) -> ( J |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
21 16 17 20 syl2anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( J |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
22 21 eqcomd 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( MetOpen ` ( D |` ( Y X. Y ) ) ) = ( J |`t Y ) )
23 metxmet 
 |-  ( ( D |` ( Y X. Y ) ) e. ( Met ` Y ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
24 14 23 syl 
 |-  ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
25 cfilfil 
 |-  ( ( ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> f e. ( Fil ` Y ) )
26 24 25 sylan 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> f e. ( Fil ` Y ) )
27 elfvdm 
 |-  ( D e. ( CMet ` X ) -> X e. dom CMet )
28 27 ad2antrr 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> X e. dom CMet )
29 trfg 
 |-  ( ( f e. ( Fil ` Y ) /\ Y C_ X /\ X e. dom CMet ) -> ( ( X filGen f ) |`t Y ) = f )
30 26 17 28 29 syl3anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( X filGen f ) |`t Y ) = f )
31 30 eqcomd 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> f = ( ( X filGen f ) |`t Y ) )
32 22 31 oveq12d 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim f ) = ( ( J |`t Y ) fLim ( ( X filGen f ) |`t Y ) ) )
33 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
34 16 33 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> J e. ( TopOn ` X ) )
35 filfbas 
 |-  ( f e. ( Fil ` Y ) -> f e. ( fBas ` Y ) )
36 26 35 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> f e. ( fBas ` Y ) )
37 filsspw 
 |-  ( f e. ( Fil ` Y ) -> f C_ ~P Y )
38 26 37 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> f C_ ~P Y )
39 17 sspwd 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ~P Y C_ ~P X )
40 38 39 sstrd 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> f C_ ~P X )
41 fbasweak 
 |-  ( ( f e. ( fBas ` Y ) /\ f C_ ~P X /\ X e. dom CMet ) -> f e. ( fBas ` X ) )
42 36 40 28 41 syl3anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> f e. ( fBas ` X ) )
43 fgcl 
 |-  ( f e. ( fBas ` X ) -> ( X filGen f ) e. ( Fil ` X ) )
44 42 43 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( X filGen f ) e. ( Fil ` X ) )
45 ssfg 
 |-  ( f e. ( fBas ` X ) -> f C_ ( X filGen f ) )
46 42 45 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> f C_ ( X filGen f ) )
47 filtop 
 |-  ( f e. ( Fil ` Y ) -> Y e. f )
48 26 47 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> Y e. f )
49 46 48 sseldd 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> Y e. ( X filGen f ) )
50 flimrest 
 |-  ( ( J e. ( TopOn ` X ) /\ ( X filGen f ) e. ( Fil ` X ) /\ Y e. ( X filGen f ) ) -> ( ( J |`t Y ) fLim ( ( X filGen f ) |`t Y ) ) = ( ( J fLim ( X filGen f ) ) i^i Y ) )
51 34 44 49 50 syl3anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( J |`t Y ) fLim ( ( X filGen f ) |`t Y ) ) = ( ( J fLim ( X filGen f ) ) i^i Y ) )
52 flimclsi 
 |-  ( Y e. ( X filGen f ) -> ( J fLim ( X filGen f ) ) C_ ( ( cls ` J ) ` Y ) )
53 49 52 syl 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( J fLim ( X filGen f ) ) C_ ( ( cls ` J ) ` Y ) )
54 cldcls 
 |-  ( Y e. ( Clsd ` J ) -> ( ( cls ` J ) ` Y ) = Y )
55 54 ad2antlr 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( cls ` J ) ` Y ) = Y )
56 53 55 sseqtrd 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( J fLim ( X filGen f ) ) C_ Y )
57 df-ss 
 |-  ( ( J fLim ( X filGen f ) ) C_ Y <-> ( ( J fLim ( X filGen f ) ) i^i Y ) = ( J fLim ( X filGen f ) ) )
58 56 57 sylib 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( J fLim ( X filGen f ) ) i^i Y ) = ( J fLim ( X filGen f ) ) )
59 32 51 58 3eqtrd 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim f ) = ( J fLim ( X filGen f ) ) )
60 simpll 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> D e. ( CMet ` X ) )
61 5 9 syl 
 |-  ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) -> D e. ( *Met ` X ) )
62 cfilresi 
 |-  ( ( D e. ( *Met ` X ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( X filGen f ) e. ( CauFil ` D ) )
63 61 62 sylan 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( X filGen f ) e. ( CauFil ` D ) )
64 1 cmetcvg 
 |-  ( ( D e. ( CMet ` X ) /\ ( X filGen f ) e. ( CauFil ` D ) ) -> ( J fLim ( X filGen f ) ) =/= (/) )
65 60 63 64 syl2anc 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( J fLim ( X filGen f ) ) =/= (/) )
66 59 65 eqnetrd 
 |-  ( ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) /\ f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim f ) =/= (/) )
67 66 ralrimiva 
 |-  ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) -> A. f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim f ) =/= (/) )
68 19 iscmet 
 |-  ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> ( ( D |` ( Y X. Y ) ) e. ( Met ` Y ) /\ A. f e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim f ) =/= (/) ) )
69 14 67 68 sylanbrc 
 |-  ( ( D e. ( CMet ` X ) /\ Y e. ( Clsd ` J ) ) -> ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) )
70 4 69 impbida 
 |-  ( D e. ( CMet ` X ) -> ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> Y e. ( Clsd ` J ) ) )