Metamath Proof Explorer

Theorem cmssmscld

Description: The restriction of a metric space is closed if it is complete. (Contributed by AV, 9-Oct-2022)

Ref Expression
Hypotheses cmsss.h 
|- K = ( M |`s A )
cmsss.x 
|- X = ( Base ` M )
cmsss.j 
|- J = ( TopOpen ` M )
Assertion cmssmscld 
|- ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> A e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 cmsss.h 
 |-  K = ( M |`s A )
2 cmsss.x 
 |-  X = ( Base ` M )
3 cmsss.j 
 |-  J = ( TopOpen ` M )
4 eqid 
 |-  ( ( dist ` M ) |` ( X X. X ) ) = ( ( dist ` M ) |` ( X X. X ) )
5 2 4 msmet 
 |-  ( M e. MetSp -> ( ( dist ` M ) |` ( X X. X ) ) e. ( Met ` X ) )
6 5 3ad2ant1 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> ( ( dist ` M ) |` ( X X. X ) ) e. ( Met ` X ) )
7 xpss12 
 |-  ( ( A C_ X /\ A C_ X ) -> ( A X. A ) C_ ( X X. X ) )
8 7 anidms 
 |-  ( A C_ X -> ( A X. A ) C_ ( X X. X ) )
9 8 3ad2ant2 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> ( A X. A ) C_ ( X X. X ) )
10 9 resabs1d 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> ( ( ( dist ` M ) |` ( X X. X ) ) |` ( A X. A ) ) = ( ( dist ` M ) |` ( A X. A ) ) )
11 2 sseq2i 
 |-  ( A C_ X <-> A C_ ( Base ` M ) )
12 fvex 
 |-  ( Base ` M ) e. _V
13 12 ssex 
 |-  ( A C_ ( Base ` M ) -> A e. _V )
14 11 13 sylbi 
 |-  ( A C_ X -> A e. _V )
15 14 3ad2ant2 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> A e. _V )
16 eqid 
 |-  ( dist ` M ) = ( dist ` M )
17 1 16 ressds 
 |-  ( A e. _V -> ( dist ` M ) = ( dist ` K ) )
18 15 17 syl 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> ( dist ` M ) = ( dist ` K ) )
19 18 reseq1d 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> ( ( dist ` M ) |` ( A X. A ) ) = ( ( dist ` K ) |` ( A X. A ) ) )
20 10 19 eqtrd 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> ( ( ( dist ` M ) |` ( X X. X ) ) |` ( A X. A ) ) = ( ( dist ` K ) |` ( A X. A ) ) )
21 eqid 
 |-  ( Base ` K ) = ( Base ` K )
22 eqid 
 |-  ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
23 21 22 iscms 
 |-  ( K e. CMetSp <-> ( K e. MetSp /\ ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( CMet ` ( Base ` K ) ) ) )
24 1 2 ressbas2 
 |-  ( A C_ X -> A = ( Base ` K ) )
25 24 adantr 
 |-  ( ( A C_ X /\ K e. MetSp ) -> A = ( Base ` K ) )
26 25 eqcomd 
 |-  ( ( A C_ X /\ K e. MetSp ) -> ( Base ` K ) = A )
27 26 sqxpeqd 
 |-  ( ( A C_ X /\ K e. MetSp ) -> ( ( Base ` K ) X. ( Base ` K ) ) = ( A X. A ) )
28 27 reseq2d 
 |-  ( ( A C_ X /\ K e. MetSp ) -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( A X. A ) ) )
29 26 fveq2d 
 |-  ( ( A C_ X /\ K e. MetSp ) -> ( CMet ` ( Base ` K ) ) = ( CMet ` A ) )
30 28 29 eleq12d 
 |-  ( ( A C_ X /\ K e. MetSp ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( CMet ` ( Base ` K ) ) <-> ( ( dist ` K ) |` ( A X. A ) ) e. ( CMet ` A ) ) )
31 30 biimpd 
 |-  ( ( A C_ X /\ K e. MetSp ) -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( CMet ` ( Base ` K ) ) -> ( ( dist ` K ) |` ( A X. A ) ) e. ( CMet ` A ) ) )
32 31 expimpd 
 |-  ( A C_ X -> ( ( K e. MetSp /\ ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( CMet ` ( Base ` K ) ) ) -> ( ( dist ` K ) |` ( A X. A ) ) e. ( CMet ` A ) ) )
33 23 32 syl5bi 
 |-  ( A C_ X -> ( K e. CMetSp -> ( ( dist ` K ) |` ( A X. A ) ) e. ( CMet ` A ) ) )
34 33 imp 
 |-  ( ( A C_ X /\ K e. CMetSp ) -> ( ( dist ` K ) |` ( A X. A ) ) e. ( CMet ` A ) )
35 34 3adant1 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> ( ( dist ` K ) |` ( A X. A ) ) e. ( CMet ` A ) )
36 20 35 eqeltrd 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> ( ( ( dist ` M ) |` ( X X. X ) ) |` ( A X. A ) ) e. ( CMet ` A ) )
37 eqid 
 |-  ( MetOpen ` ( ( dist ` M ) |` ( X X. X ) ) ) = ( MetOpen ` ( ( dist ` M ) |` ( X X. X ) ) )
38 37 metsscmetcld 
 |-  ( ( ( ( dist ` M ) |` ( X X. X ) ) e. ( Met ` X ) /\ ( ( ( dist ` M ) |` ( X X. X ) ) |` ( A X. A ) ) e. ( CMet ` A ) ) -> A e. ( Clsd ` ( MetOpen ` ( ( dist ` M ) |` ( X X. X ) ) ) ) )
39 6 36 38 syl2anc 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> A e. ( Clsd ` ( MetOpen ` ( ( dist ` M ) |` ( X X. X ) ) ) ) )
40 3 2 4 mstopn 
 |-  ( M e. MetSp -> J = ( MetOpen ` ( ( dist ` M ) |` ( X X. X ) ) ) )
41 40 3ad2ant1 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> J = ( MetOpen ` ( ( dist ` M ) |` ( X X. X ) ) ) )
42 41 fveq2d 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> ( Clsd ` J ) = ( Clsd ` ( MetOpen ` ( ( dist ` M ) |` ( X X. X ) ) ) ) )
43 39 42 eleqtrrd 
 |-  ( ( M e. MetSp /\ A C_ X /\ K e. CMetSp ) -> A e. ( Clsd ` J ) )