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 ⊢ 𝐾 = ( 𝑀 ↾s 𝐴 )
cmsss.x ⊢ 𝑋 = ( Base ‘ 𝑀 )
cmsss.j ⊢ 𝐽 = ( TopOpen ‘ 𝑀 )
Assertion cmssmscld ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 cmsss.h ⊢ 𝐾 = ( 𝑀 ↾s 𝐴 )
2 cmsss.x ⊢ 𝑋 = ( Base ‘ 𝑀 )
3 cmsss.j ⊢ 𝐽 = ( TopOpen ‘ 𝑀 )
4 eqid ⊢ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) )
5 2 4 msmet ⊢ ( 𝑀 ∈ MetSp → ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) )
6 5 3ad2ant1 ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) )
7 xpss12 ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋 ) → ( 𝐴 × 𝐴 ) ⊆ ( 𝑋 × 𝑋 ) )
8 7 anidms ⊢ ( 𝐴 ⊆ 𝑋 → ( 𝐴 × 𝐴 ) ⊆ ( 𝑋 × 𝑋 ) )
9 8 3ad2ant2 ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( 𝐴 × 𝐴 ) ⊆ ( 𝑋 × 𝑋 ) )
10 9 resabs1d ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝑀 ) ↾ ( 𝐴 × 𝐴 ) ) )
11 2 sseq2i ⊢ ( 𝐴 ⊆ 𝑋 ↔ 𝐴 ⊆ ( Base ‘ 𝑀 ) )
12 fvex ⊢ ( Base ‘ 𝑀 ) ∈ V
13 12 ssex ⊢ ( 𝐴 ⊆ ( Base ‘ 𝑀 ) → 𝐴 ∈ V )
14 11 13 sylbi ⊢ ( 𝐴 ⊆ 𝑋 → 𝐴 ∈ V )
15 14 3ad2ant2 ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → 𝐴 ∈ V )
16 eqid ⊢ ( dist ‘ 𝑀 ) = ( dist ‘ 𝑀 )
17 1 16 ressds ⊢ ( 𝐴 ∈ V → ( dist ‘ 𝑀 ) = ( dist ‘ 𝐾 ) )
18 15 17 syl ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( dist ‘ 𝑀 ) = ( dist ‘ 𝐾 ) )
19 18 reseq1d ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( ( dist ‘ 𝑀 ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( 𝐴 × 𝐴 ) ) )
20 10 19 eqtrd ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝐴 × 𝐴 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( 𝐴 × 𝐴 ) ) )
21 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
22 eqid ⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
23 21 22 iscms ⊢ ( 𝐾 ∈ CMetSp ↔ ( 𝐾 ∈ MetSp ∧ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ) )
24 1 2 ressbas2 ⊢ ( 𝐴 ⊆ 𝑋 → 𝐴 = ( Base ‘ 𝐾 ) )
25 24 adantr ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ MetSp ) → 𝐴 = ( Base ‘ 𝐾 ) )
26 25 eqcomd ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ MetSp ) → ( Base ‘ 𝐾 ) = 𝐴 )
27 26 sqxpeqd ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ MetSp ) → ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) = ( 𝐴 × 𝐴 ) )
28 27 reseq2d ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ MetSp ) → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( 𝐴 × 𝐴 ) ) )
29 26 fveq2d ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ MetSp ) → ( CMet ‘ ( Base ‘ 𝐾 ) ) = ( CMet ‘ 𝐴 ) )
30 28 29 eleq12d ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ MetSp ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ↔ ( ( dist ‘ 𝐾 ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) ) )
31 30 biimpd ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ MetSp ) → ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) → ( ( dist ‘ 𝐾 ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) ) )
32 31 expimpd ⊢ ( 𝐴 ⊆ 𝑋 → ( ( 𝐾 ∈ MetSp ∧ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( CMet ‘ ( Base ‘ 𝐾 ) ) ) → ( ( dist ‘ 𝐾 ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) ) )
33 23 32 biimtrid ⊢ ( 𝐴 ⊆ 𝑋 → ( 𝐾 ∈ CMetSp → ( ( dist ‘ 𝐾 ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) ) )
34 33 imp ⊢ ( ( 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( ( dist ‘ 𝐾 ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) )
35 34 3adant1 ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( ( dist ‘ 𝐾 ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) )
36 20 35 eqeltrd ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) )
37 eqid ⊢ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) = ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
38 37 metsscmetcld ⊢ ( ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ∈ ( Met ‘ 𝑋 ) ∧ ( ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ↾ ( 𝐴 × 𝐴 ) ) ∈ ( CMet ‘ 𝐴 ) ) → 𝐴 ∈ ( Clsd ‘ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) ) )
39 6 36 38 syl2anc ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → 𝐴 ∈ ( Clsd ‘ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) ) )
40 3 2 4 mstopn ⊢ ( 𝑀 ∈ MetSp → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) )
41 40 3ad2ant1 ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → 𝐽 = ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) )
42 41 fveq2d ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → ( Clsd ‘ 𝐽 ) = ( Clsd ‘ ( MetOpen ‘ ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) ) ) )
43 39 42 eleqtrrd ⊢ ( ( 𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp ) → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )