cmetss

Description: A subspace of a complete metric space is complete iff it is closed in the parent space. Theorem 1.4-7 of Kreyszig p. 30. (Contributed by NM, 28-Jan-2008) (Revised by Mario Carneiro, 15-Oct-2015) (Proof shortened by AV, 9-Oct-2022)

		Ref	Expression
	Hypothesis	metsscmetcld.j	$⊢ J = MetOpen (D)$
	Assertion	cmetss	$⊢ D \in CMet (X) \to ({D ↾}_{(Y \times Y)} \in CMet (Y) \leftrightarrow Y \in Clsd (J))$

Proof

Step	Hyp	Ref	Expression
1		metsscmetcld.j	$⊢ J = MetOpen (D)$
2		cmetmet	$⊢ D \in CMet (X) \to D \in Met (X)$
3	1	metsscmetcld	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to Y \in Clsd (J)$
4	2 3	sylan	$⊢ (D \in CMet (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to Y \in Clsd (J)$
5	2	adantr	$⊢ (D \in CMet (X) \land Y \in Clsd (J)) \to D \in Met (X)$
6		eqid	$⊢ ⋃ J = ⋃ J$
7	6	cldss	$⊢ Y \in Clsd (J) \to Y \subseteq ⋃ J$
8	7	adantl	$⊢ (D \in CMet (X) \land Y \in Clsd (J)) \to Y \subseteq ⋃ J$
9		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
10	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
11	5 9 10	3syl	$⊢ (D \in CMet (X) \land Y \in Clsd (J)) \to X = ⋃ J$
12	8 11	sseqtrrd	$⊢ (D \in CMet (X) \land Y \in Clsd (J)) \to Y \subseteq X$
13		metres2	$⊢ (D \in Met (X) \land Y \subseteq X) \to {D ↾}_{(Y \times Y)} \in Met (Y)$
14	5 12 13	syl2anc	$⊢ (D \in CMet (X) \land Y \in Clsd (J)) \to {D ↾}_{(Y \times Y)} \in Met (Y)$
15	2 9	syl	$⊢ D \in CMet (X) \to D \in ∞Met (X)$
16	15	ad2antrr	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to D \in ∞Met (X)$
17	12	adantr	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to Y \subseteq X$
18		eqid	$⊢ {D ↾}_{(Y \times Y)} = {D ↾}_{(Y \times Y)}$
19		eqid	$⊢ MetOpen ({D ↾}_{(Y \times Y)}) = MetOpen ({D ↾}_{(Y \times Y)})$
20	18 1 19	metrest	$⊢ (D \in ∞Met (X) \land Y \subseteq X) \to J ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
21	16 17 20	syl2anc	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to J ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
22	21	eqcomd	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to MetOpen ({D ↾}_{(Y \times Y)}) = J ↾_{𝑡} Y$
23		metxmet	$⊢ {D ↾}_{(Y \times Y)} \in Met (Y) \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
24	14 23	syl	$⊢ (D \in CMet (X) \land Y \in Clsd (J)) \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
25		cfilfil	$⊢ ({D ↾}_{(Y \times Y)} \in ∞Met (Y) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to f \in Fil (Y)$
26	24 25	sylan	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to f \in Fil (Y)$
27		elfvdm	$⊢ D \in CMet (X) \to X \in dom CMet$
28	27	ad2antrr	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to X \in dom CMet$
29		trfg	$⊢ (f \in Fil (Y) \land Y \subseteq X \land X \in dom CMet) \to (X filGen f) ↾_{𝑡} Y = f$
30	26 17 28 29	syl3anc	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to (X filGen f) ↾_{𝑡} Y = f$
31	30	eqcomd	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to f = (X filGen f) ↾_{𝑡} Y$
32	22 31	oveq12d	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to MetOpen ({D ↾}_{(Y \times Y)}) fLim f = (J ↾_{𝑡} Y) fLim ((X filGen f) ↾_{𝑡} Y)$
33	1	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
34	16 33	syl	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to J \in TopOn (X)$
35		filfbas	$⊢ f \in Fil (Y) \to f \in fBas (Y)$
36	26 35	syl	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to f \in fBas (Y)$
37		filsspw	$⊢ f \in Fil (Y) \to f \subseteq 𝒫 Y$
38	26 37	syl	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to f \subseteq 𝒫 Y$
39	17	sspwd	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to 𝒫 Y \subseteq 𝒫 X$
40	38 39	sstrd	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to f \subseteq 𝒫 X$
41		fbasweak	$⊢ (f \in fBas (Y) \land f \subseteq 𝒫 X \land X \in dom CMet) \to f \in fBas (X)$
42	36 40 28 41	syl3anc	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to f \in fBas (X)$
43		fgcl	$⊢ f \in fBas (X) \to X filGen f \in Fil (X)$
44	42 43	syl	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to X filGen f \in Fil (X)$
45		ssfg	$⊢ f \in fBas (X) \to f \subseteq X filGen f$
46	42 45	syl	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to f \subseteq X filGen f$
47		filtop	$⊢ f \in Fil (Y) \to Y \in f$
48	26 47	syl	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to Y \in f$
49	46 48	sseldd	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to Y \in (X filGen f)$
50		flimrest	$⊢ (J \in TopOn (X) \land X filGen f \in Fil (X) \land Y \in (X filGen f)) \to (J ↾_{𝑡} Y) fLim ((X filGen f) ↾_{𝑡} Y) = (J fLim (X filGen f)) \cap Y$
51	34 44 49 50	syl3anc	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to (J ↾_{𝑡} Y) fLim ((X filGen f) ↾_{𝑡} Y) = (J fLim (X filGen f)) \cap Y$
52		flimclsi	$⊢ Y \in (X filGen f) \to J fLim (X filGen f) \subseteq cls (J) (Y)$
53	49 52	syl	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to J fLim (X filGen f) \subseteq cls (J) (Y)$
54		cldcls	$⊢ Y \in Clsd (J) \to cls (J) (Y) = Y$
55	54	ad2antlr	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to cls (J) (Y) = Y$
56	53 55	sseqtrd	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to J fLim (X filGen f) \subseteq Y$
57		df-ss	$⊢ J fLim (X filGen f) \subseteq Y \leftrightarrow (J fLim (X filGen f)) \cap Y = J fLim (X filGen f)$
58	56 57	sylib	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to (J fLim (X filGen f)) \cap Y = J fLim (X filGen f)$
59	32 51 58	3eqtrd	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to MetOpen ({D ↾}_{(Y \times Y)}) fLim f = J fLim (X filGen f)$
60		simpll	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to D \in CMet (X)$
61	5 9	syl	$⊢ (D \in CMet (X) \land Y \in Clsd (J)) \to D \in ∞Met (X)$
62		cfilresi	$⊢ (D \in ∞Met (X) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to X filGen f \in CauFil (D)$
63	61 62	sylan	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to X filGen f \in CauFil (D)$
64	1	cmetcvg	$⊢ (D \in CMet (X) \land X filGen f \in CauFil (D)) \to J fLim (X filGen f) \neq \emptyset$
65	60 63 64	syl2anc	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to J fLim (X filGen f) \neq \emptyset$
66	59 65	eqnetrd	$⊢ ((D \in CMet (X) \land Y \in Clsd (J)) \land f \in CauFil ({D ↾}_{(Y \times Y)})) \to MetOpen ({D ↾}_{(Y \times Y)}) fLim f \neq \emptyset$
67	66	ralrimiva	$⊢ (D \in CMet (X) \land Y \in Clsd (J)) \to \forall f \in CauFil ({D ↾}_{(Y \times Y)}) MetOpen ({D ↾}_{(Y \times Y)}) fLim f \neq \emptyset$
68	19	iscmet	$⊢ {D ↾}_{(Y \times Y)} \in CMet (Y) \leftrightarrow ({D ↾}_{(Y \times Y)} \in Met (Y) \land \forall f \in CauFil ({D ↾}_{(Y \times Y)}) MetOpen ({D ↾}_{(Y \times Y)}) fLim f \neq \emptyset)$
69	14 67 68	sylanbrc	$⊢ (D \in CMet (X) \land Y \in Clsd (J)) \to {D ↾}_{(Y \times Y)} \in CMet (Y)$
70	4 69	impbida	$⊢ D \in CMet (X) \to ({D ↾}_{(Y \times Y)} \in CMet (Y) \leftrightarrow Y \in Clsd (J))$

Metamath Proof Explorer

Theorem cmetss

Proof