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 ↾ 𝑠 A
cmsss.x ⊢ X = Base M
cmsss.j ⊢ J = TopOpen ⁡ M
Assertion cmssmscld ⊢ M ∈ MetSp ∧ A ⊆ X ∧ K ∈ CMetSp → A ∈ Clsd ⁡ J

Proof

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