Metamath Proof Explorer

Theorem metsscmetcld

Description: A complete subspace of a metric space is closed in the parent space. Formerly part of proof for cmetss . (Contributed by NM, 28-Jan-2008) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 9-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 metsscmetcld.j 
 |-  J = ( MetOpen ` D )
2 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
3 2 adantr 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> D e. ( *Met ` X ) )
4 1 mopntopon 
 |-  ( D e. ( *Met ` X ) -> J e. ( TopOn ` X ) )
5 3 4 syl 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> J e. ( TopOn ` X ) )
6 resss 
 |-  ( D |` ( Y X. Y ) ) C_ D
7 dmss 
 |-  ( ( D |` ( Y X. Y ) ) C_ D -> dom ( D |` ( Y X. Y ) ) C_ dom D )
8 dmss 
 |-  ( dom ( D |` ( Y X. Y ) ) C_ dom D -> dom dom ( D |` ( Y X. Y ) ) C_ dom dom D )
9 6 7 8 mp2b 
 |-  dom dom ( D |` ( Y X. Y ) ) C_ dom dom D
10 cmetmet 
 |-  ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) -> ( D |` ( Y X. Y ) ) e. ( Met ` Y ) )
11 metdmdm 
 |-  ( ( D |` ( Y X. Y ) ) e. ( Met ` Y ) -> Y = dom dom ( D |` ( Y X. Y ) ) )
12 10 11 syl 
 |-  ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) -> Y = dom dom ( D |` ( Y X. Y ) ) )
13 metdmdm 
 |-  ( D e. ( Met ` X ) -> X = dom dom D )
14 sseq12 
 |-  ( ( Y = dom dom ( D |` ( Y X. Y ) ) /\ X = dom dom D ) -> ( Y C_ X <-> dom dom ( D |` ( Y X. Y ) ) C_ dom dom D ) )
15 12 13 14 syl2anr 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> ( Y C_ X <-> dom dom ( D |` ( Y X. Y ) ) C_ dom dom D ) )
16 9 15 mpbiri 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> Y C_ X )
17 flimcls 
 |-  ( ( J e. ( TopOn ` X ) /\ Y C_ X ) -> ( x e. ( ( cls ` J ) ` Y ) <-> E. f e. ( Fil ` X ) ( Y e. f /\ x e. ( J fLim f ) ) ) )
18 5 16 17 syl2anc 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> ( x e. ( ( cls ` J ) ` Y ) <-> E. f e. ( Fil ` X ) ( Y e. f /\ x e. ( J fLim f ) ) ) )
19 simprrr 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> x e. ( J fLim f ) )
20 3 adantr 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> D e. ( *Met ` X ) )
21 1 methaus 
 |-  ( D e. ( *Met ` X ) -> J e. Haus )
22 hausflimi 
 |-  ( J e. Haus -> E* x x e. ( J fLim f ) )
23 20 21 22 3syl 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> E* x x e. ( J fLim f ) )
24 20 4 syl 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> J e. ( TopOn ` X ) )
25 simprl 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> f e. ( Fil ` X ) )
26 simprrl 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> Y e. f )
27 flimrest 
 |-  ( ( J e. ( TopOn ` X ) /\ f e. ( Fil ` X ) /\ Y e. f ) -> ( ( J |`t Y ) fLim ( f |`t Y ) ) = ( ( J fLim f ) i^i Y ) )
28 24 25 26 27 syl3anc 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( ( J |`t Y ) fLim ( f |`t Y ) ) = ( ( J fLim f ) i^i Y ) )
29 16 adantr 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> Y C_ X )
30 eqid 
 |-  ( D |` ( Y X. Y ) ) = ( D |` ( Y X. Y ) )
31 eqid 
 |-  ( MetOpen ` ( D |` ( Y X. Y ) ) ) = ( MetOpen ` ( D |` ( Y X. Y ) ) )
32 30 1 31 metrest 
 |-  ( ( D e. ( *Met ` X ) /\ Y C_ X ) -> ( J |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
33 20 29 32 syl2anc 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( J |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
34 33 oveq1d 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( ( J |`t Y ) fLim ( f |`t Y ) ) = ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim ( f |`t Y ) ) )
35 28 34 eqtr3d 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( ( J fLim f ) i^i Y ) = ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim ( f |`t Y ) ) )
36 simplr 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) )
37 1 flimcfil 
 |-  ( ( D e. ( *Met ` X ) /\ x e. ( J fLim f ) ) -> f e. ( CauFil ` D ) )
38 20 19 37 syl2anc 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> f e. ( CauFil ` D ) )
39 cfilres 
 |-  ( ( D e. ( *Met ` X ) /\ f e. ( Fil ` X ) /\ Y e. f ) -> ( f e. ( CauFil ` D ) <-> ( f |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) )
40 20 25 26 39 syl3anc 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( f e. ( CauFil ` D ) <-> ( f |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) )
41 38 40 mpbid 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( f |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) )
42 31 cmetcvg 
 |-  ( ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) /\ ( f |`t Y ) e. ( CauFil ` ( D |` ( Y X. Y ) ) ) ) -> ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim ( f |`t Y ) ) =/= (/) )
43 36 41 42 syl2anc 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) fLim ( f |`t Y ) ) =/= (/) )
44 35 43 eqnetrd 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( ( J fLim f ) i^i Y ) =/= (/) )
45 ndisj 
 |-  ( ( ( J fLim f ) i^i Y ) =/= (/) <-> E. x ( x e. ( J fLim f ) /\ x e. Y ) )
46 44 45 sylib 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> E. x ( x e. ( J fLim f ) /\ x e. Y ) )
47 mopick 
 |-  ( ( E* x x e. ( J fLim f ) /\ E. x ( x e. ( J fLim f ) /\ x e. Y ) ) -> ( x e. ( J fLim f ) -> x e. Y ) )
48 23 46 47 syl2anc 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> ( x e. ( J fLim f ) -> x e. Y ) )
49 19 48 mpd 
 |-  ( ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) /\ ( f e. ( Fil ` X ) /\ ( Y e. f /\ x e. ( J fLim f ) ) ) ) -> x e. Y )
50 49 rexlimdvaa 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> ( E. f e. ( Fil ` X ) ( Y e. f /\ x e. ( J fLim f ) ) -> x e. Y ) )
51 18 50 sylbid 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> ( x e. ( ( cls ` J ) ` Y ) -> x e. Y ) )
52 51 ssrdv 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> ( ( cls ` J ) ` Y ) C_ Y )
53 1 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
54 3 53 syl 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> J e. Top )
55 1 mopnuni 
 |-  ( D e. ( *Met ` X ) -> X = U. J )
56 3 55 syl 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> X = U. J )
57 16 56 sseqtrd 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> Y C_ U. J )
58 eqid 
 |-  U. J = U. J
59 58 iscld4 
 |-  ( ( J e. Top /\ Y C_ U. J ) -> ( Y e. ( Clsd ` J ) <-> ( ( cls ` J ) ` Y ) C_ Y ) )
60 54 57 59 syl2anc 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> ( Y e. ( Clsd ` J ) <-> ( ( cls ` J ) ` Y ) C_ Y ) )
61 52 60 mpbird 
 |-  ( ( D e. ( Met ` X ) /\ ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) -> Y e. ( Clsd ` J ) )