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 \in MetSp \land A \subseteq X \land K \in CMetSp) \to A \in 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 \times X)} = {dist (M) ↾}_{(X \times X)}$
5	2 4	msmet	$⊢ M \in MetSp \to {dist (M) ↾}_{(X \times X)} \in Met (X)$
6	5	3ad2ant1	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to {dist (M) ↾}_{(X \times X)} \in Met (X)$
7		xpss12	$⊢ (A \subseteq X \land A \subseteq X) \to A \times A \subseteq X \times X$
8	7	anidms	$⊢ A \subseteq X \to A \times A \subseteq X \times X$
9	8	3ad2ant2	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to A \times A \subseteq X \times X$
10	9	resabs1d	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to {({dist (M) ↾}_{(X \times X)}) ↾}_{(A \times A)} = {dist (M) ↾}_{(A \times A)}$
11	2	sseq2i	$⊢ A \subseteq X \leftrightarrow A \subseteq {Base}_{M}$
12		fvex	$⊢ {Base}_{M} \in V$
13	12	ssex	$⊢ A \subseteq {Base}_{M} \to A \in V$
14	11 13	sylbi	$⊢ A \subseteq X \to A \in V$
15	14	3ad2ant2	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to A \in V$
16		eqid	$⊢ dist (M) = dist (M)$
17	1 16	ressds	$⊢ A \in V \to dist (M) = dist (K)$
18	15 17	syl	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to dist (M) = dist (K)$
19	18	reseq1d	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to {dist (M) ↾}_{(A \times A)} = {dist (K) ↾}_{(A \times A)}$
20	10 19	eqtrd	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to {({dist (M) ↾}_{(X \times X)}) ↾}_{(A \times A)} = {dist (K) ↾}_{(A \times A)}$
21		eqid	$⊢ {Base}_{K} = {Base}_{K}$
22		eqid	$⊢ {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} = {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})}$
23	21 22	iscms	$⊢ K \in CMetSp \leftrightarrow (K \in MetSp \land {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in CMet ({Base}_{K}))$
24	1 2	ressbas2	$⊢ A \subseteq X \to A = {Base}_{K}$
25	24	adantr	$⊢ (A \subseteq X \land K \in MetSp) \to A = {Base}_{K}$
26	25	eqcomd	$⊢ (A \subseteq X \land K \in MetSp) \to {Base}_{K} = A$
27	26	sqxpeqd	$⊢ (A \subseteq X \land K \in MetSp) \to {Base}_{K} \times {Base}_{K} = A \times A$
28	27	reseq2d	$⊢ (A \subseteq X \land K \in MetSp) \to {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} = {dist (K) ↾}_{(A \times A)}$
29	26	fveq2d	$⊢ (A \subseteq X \land K \in MetSp) \to CMet ({Base}_{K}) = CMet (A)$
30	28 29	eleq12d	$⊢ (A \subseteq X \land K \in MetSp) \to ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in CMet ({Base}_{K}) \leftrightarrow {dist (K) ↾}_{(A \times A)} \in CMet (A))$
31	30	biimpd	$⊢ (A \subseteq X \land K \in MetSp) \to ({dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in CMet ({Base}_{K}) \to {dist (K) ↾}_{(A \times A)} \in CMet (A))$
32	31	expimpd	$⊢ A \subseteq X \to ((K \in MetSp \land {dist (K) ↾}_{({Base}_{K} \times {Base}_{K})} \in CMet ({Base}_{K})) \to {dist (K) ↾}_{(A \times A)} \in CMet (A))$
33	23 32	biimtrid	$⊢ A \subseteq X \to (K \in CMetSp \to {dist (K) ↾}_{(A \times A)} \in CMet (A))$
34	33	imp	$⊢ (A \subseteq X \land K \in CMetSp) \to {dist (K) ↾}_{(A \times A)} \in CMet (A)$
35	34	3adant1	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to {dist (K) ↾}_{(A \times A)} \in CMet (A)$
36	20 35	eqeltrd	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to {({dist (M) ↾}_{(X \times X)}) ↾}_{(A \times A)} \in CMet (A)$
37		eqid	$⊢ MetOpen ({dist (M) ↾}_{(X \times X)}) = MetOpen ({dist (M) ↾}_{(X \times X)})$
38	37	metsscmetcld	$⊢ ({dist (M) ↾}_{(X \times X)} \in Met (X) \land {({dist (M) ↾}_{(X \times X)}) ↾}_{(A \times A)} \in CMet (A)) \to A \in Clsd (MetOpen ({dist (M) ↾}_{(X \times X)}))$
39	6 36 38	syl2anc	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to A \in Clsd (MetOpen ({dist (M) ↾}_{(X \times X)}))$
40	3 2 4	mstopn	$⊢ M \in MetSp \to J = MetOpen ({dist (M) ↾}_{(X \times X)})$
41	40	3ad2ant1	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to J = MetOpen ({dist (M) ↾}_{(X \times X)})$
42	41	fveq2d	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to Clsd (J) = Clsd (MetOpen ({dist (M) ↾}_{(X \times X)}))$
43	39 42	eleqtrrd	$⊢ (M \in MetSp \land A \subseteq X \land K \in CMetSp) \to A \in Clsd (J)$

Metamath Proof Explorer

Theorem cmssmscld

Proof