Metamath Proof Explorer

Theorem cmsss

Description: The restriction of a complete metric space is complete iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses cmsss.h ⊢ K = M ↾ 𝑠 A
cmsss.x ⊢ X = Base M
cmsss.j ⊢ J = TopOpen ⁡ M
Assertion cmsss ⊢ M ∈ CMetSp ∧ 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 simpr ⊢ M ∈ CMetSp ∧ A ⊆ X → A ⊆ X
5 xpss12 ⊢ A ⊆ X ∧ A ⊆ X → A × A ⊆ X × X
6 4 5 sylancom ⊢ M ∈ CMetSp ∧ A ⊆ X → A × A ⊆ X × X
7 6 resabs1d ⊢ M ∈ CMetSp ∧ A ⊆ X → dist ⁡ M ↾ X × X ↾ A × A = dist ⁡ M ↾ A × A
8 2 fvexi ⊢ X ∈ V
9 8 ssex ⊢ A ⊆ X → A ∈ V
10 9 adantl ⊢ M ∈ CMetSp ∧ A ⊆ X → A ∈ V
11 eqid ⊢ dist ⁡ M = dist ⁡ M
12 1 11 ressds ⊢ A ∈ V → dist ⁡ M = dist ⁡ K
13 10 12 syl ⊢ M ∈ CMetSp ∧ A ⊆ X → dist ⁡ M = dist ⁡ K
14 1 2 ressbas2 ⊢ A ⊆ X → A = Base K
15 14 adantl ⊢ M ∈ CMetSp ∧ A ⊆ X → A = Base K
16 15 sqxpeqd ⊢ M ∈ CMetSp ∧ A ⊆ X → A × A = Base K × Base K
17 13 16 reseq12d ⊢ M ∈ CMetSp ∧ A ⊆ X → dist ⁡ M ↾ A × A = dist ⁡ K ↾ Base K × Base K
18 7 17 eqtrd ⊢ M ∈ CMetSp ∧ A ⊆ X → dist ⁡ M ↾ X × X ↾ A × A = dist ⁡ K ↾ Base K × Base K
19 15 fveq2d ⊢ M ∈ CMetSp ∧ A ⊆ X → CMet ⁡ A = CMet ⁡ Base K
20 18 19 eleq12d ⊢ M ∈ CMetSp ∧ A ⊆ X → dist ⁡ M ↾ X × X ↾ A × A ∈ CMet ⁡ A ↔ dist ⁡ K ↾ Base K × Base K ∈ CMet ⁡ Base K
21 eqid ⊢ dist ⁡ M ↾ X × X = dist ⁡ M ↾ X × X
22 2 21 cmscmet ⊢ M ∈ CMetSp → dist ⁡ M ↾ X × X ∈ CMet ⁡ X
23 22 adantr ⊢ M ∈ CMetSp ∧ A ⊆ X → dist ⁡ M ↾ X × X ∈ CMet ⁡ X
24 eqid ⊢ MetOpen ⁡ dist ⁡ M ↾ X × X = MetOpen ⁡ dist ⁡ M ↾ X × X
25 24 cmetss ⊢ dist ⁡ M ↾ X × X ∈ CMet ⁡ X → dist ⁡ M ↾ X × X ↾ A × A ∈ CMet ⁡ A ↔ A ∈ Clsd ⁡ MetOpen ⁡ dist ⁡ M ↾ X × X
26 23 25 syl ⊢ M ∈ CMetSp ∧ A ⊆ X → dist ⁡ M ↾ X × X ↾ A × A ∈ CMet ⁡ A ↔ A ∈ Clsd ⁡ MetOpen ⁡ dist ⁡ M ↾ X × X
27 20 26 bitr3d ⊢ M ∈ CMetSp ∧ A ⊆ X → dist ⁡ K ↾ Base K × Base K ∈ CMet ⁡ Base K ↔ A ∈ Clsd ⁡ MetOpen ⁡ dist ⁡ M ↾ X × X
28 cmsms ⊢ M ∈ CMetSp → M ∈ MetSp
29 ressms ⊢ M ∈ MetSp ∧ A ∈ V → M ↾ 𝑠 A ∈ MetSp
30 1 29 eqeltrid ⊢ M ∈ MetSp ∧ A ∈ V → K ∈ MetSp
31 28 9 30 syl2an ⊢ M ∈ CMetSp ∧ A ⊆ X → K ∈ MetSp
32 eqid ⊢ Base K = Base K
33 eqid ⊢ dist ⁡ K ↾ Base K × Base K = dist ⁡ K ↾ Base K × Base K
34 32 33 iscms ⊢ K ∈ CMetSp ↔ K ∈ MetSp ∧ dist ⁡ K ↾ Base K × Base K ∈ CMet ⁡ Base K
35 34 baib ⊢ K ∈ MetSp → K ∈ CMetSp ↔ dist ⁡ K ↾ Base K × Base K ∈ CMet ⁡ Base K
36 31 35 syl ⊢ M ∈ CMetSp ∧ A ⊆ X → K ∈ CMetSp ↔ dist ⁡ K ↾ Base K × Base K ∈ CMet ⁡ Base K
37 28 adantr ⊢ M ∈ CMetSp ∧ A ⊆ X → M ∈ MetSp
38 3 2 21 mstopn ⊢ M ∈ MetSp → J = MetOpen ⁡ dist ⁡ M ↾ X × X
39 37 38 syl ⊢ M ∈ CMetSp ∧ A ⊆ X → J = MetOpen ⁡ dist ⁡ M ↾ X × X
40 39 fveq2d ⊢ M ∈ CMetSp ∧ A ⊆ X → Clsd ⁡ J = Clsd ⁡ MetOpen ⁡ dist ⁡ M ↾ X × X
41 40 eleq2d ⊢ M ∈ CMetSp ∧ A ⊆ X → A ∈ Clsd ⁡ J ↔ A ∈ Clsd ⁡ MetOpen ⁡ dist ⁡ M ↾ X × X
42 27 36 41 3bitr4d ⊢ M ∈ CMetSp ∧ A ⊆ X → K ∈ CMetSp ↔ A ∈ Clsd ⁡ J