metsscmetcld

Description: A complete subspace of a metric space is closed in the parent space. Formerly part of proof for cmetss . (Contributed by NM, 28-Jan-2008) (Revised by Mario Carneiro, 15-Oct-2015) (Revised by AV, 9-Oct-2022)

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

Proof

Step	Hyp	Ref	Expression
1		metsscmetcld.j	$⊢ J = MetOpen (D)$
2		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
3	2	adantr	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to D \in ∞Met (X)$
4	1	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
5	3 4	syl	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to J \in TopOn (X)$
6		resss	$⊢ {D ↾}_{(Y \times Y)} \subseteq D$
7		dmss	$⊢ {D ↾}_{(Y \times Y)} \subseteq D \to dom ({D ↾}_{(Y \times Y)}) \subseteq dom D$
8		dmss	$⊢ dom ({D ↾}_{(Y \times Y)}) \subseteq dom D \to dom dom ({D ↾}_{(Y \times Y)}) \subseteq dom dom D$
9	6 7 8	mp2b	$⊢ dom dom ({D ↾}_{(Y \times Y)}) \subseteq dom dom D$
10		cmetmet	$⊢ {D ↾}_{(Y \times Y)} \in CMet (Y) \to {D ↾}_{(Y \times Y)} \in Met (Y)$
11		metdmdm	$⊢ {D ↾}_{(Y \times Y)} \in Met (Y) \to Y = dom dom ({D ↾}_{(Y \times Y)})$
12	10 11	syl	$⊢ {D ↾}_{(Y \times Y)} \in CMet (Y) \to Y = dom dom ({D ↾}_{(Y \times Y)})$
13		metdmdm	$⊢ D \in Met (X) \to X = dom dom D$
14		sseq12	$⊢ (Y = dom dom ({D ↾}_{(Y \times Y)}) \land X = dom dom D) \to (Y \subseteq X \leftrightarrow dom dom ({D ↾}_{(Y \times Y)}) \subseteq dom dom D)$
15	12 13 14	syl2anr	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to (Y \subseteq X \leftrightarrow dom dom ({D ↾}_{(Y \times Y)}) \subseteq dom dom D)$
16	9 15	mpbiri	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to Y \subseteq X$
17		flimcls	$⊢ (J \in TopOn (X) \land Y \subseteq X) \to (x \in cls (J) (Y) \leftrightarrow \exists f \in Fil (X) (Y \in f \land x \in (J fLim f)))$
18	5 16 17	syl2anc	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to (x \in cls (J) (Y) \leftrightarrow \exists f \in Fil (X) (Y \in f \land x \in (J fLim f)))$
19		simprrr	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to x \in (J fLim f)$
20	3	adantr	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to D \in ∞Met (X)$
21	1	methaus	$⊢ D \in ∞Met (X) \to J \in Haus$
22		hausflimi	$⊢ J \in Haus \to \exists^{*} x x \in (J fLim f)$
23	20 21 22	3syl	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to \exists^{*} x x \in (J fLim f)$
24	20 4	syl	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to J \in TopOn (X)$
25		simprl	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to f \in Fil (X)$
26		simprrl	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to Y \in f$
27		flimrest	$⊢ (J \in TopOn (X) \land f \in Fil (X) \land Y \in f) \to (J ↾_{𝑡} Y) fLim (f ↾_{𝑡} Y) = (J fLim f) \cap Y$
28	24 25 26 27	syl3anc	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to (J ↾_{𝑡} Y) fLim (f ↾_{𝑡} Y) = (J fLim f) \cap Y$
29	16	adantr	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to Y \subseteq X$
30		eqid	$⊢ {D ↾}_{(Y \times Y)} = {D ↾}_{(Y \times Y)}$
31		eqid	$⊢ MetOpen ({D ↾}_{(Y \times Y)}) = MetOpen ({D ↾}_{(Y \times Y)})$
32	30 1 31	metrest	$⊢ (D \in ∞Met (X) \land Y \subseteq X) \to J ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
33	20 29 32	syl2anc	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to J ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
34	33	oveq1d	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to (J ↾_{𝑡} Y) fLim (f ↾_{𝑡} Y) = MetOpen ({D ↾}_{(Y \times Y)}) fLim (f ↾_{𝑡} Y)$
35	28 34	eqtr3d	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to (J fLim f) \cap Y = MetOpen ({D ↾}_{(Y \times Y)}) fLim (f ↾_{𝑡} Y)$
36		simplr	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to {D ↾}_{(Y \times Y)} \in CMet (Y)$
37	1	flimcfil	$⊢ (D \in ∞Met (X) \land x \in (J fLim f)) \to f \in CauFil (D)$
38	20 19 37	syl2anc	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to f \in CauFil (D)$
39		cfilres	$⊢ (D \in ∞Met (X) \land f \in Fil (X) \land Y \in f) \to (f \in CauFil (D) \leftrightarrow f ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}))$
40	20 25 26 39	syl3anc	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to (f \in CauFil (D) \leftrightarrow f ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)}))$
41	38 40	mpbid	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to f ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)})$
42	31	cmetcvg	$⊢ ({D ↾}_{(Y \times Y)} \in CMet (Y) \land f ↾_{𝑡} Y \in CauFil ({D ↾}_{(Y \times Y)})) \to MetOpen ({D ↾}_{(Y \times Y)}) fLim (f ↾_{𝑡} Y) \neq \emptyset$
43	36 41 42	syl2anc	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to MetOpen ({D ↾}_{(Y \times Y)}) fLim (f ↾_{𝑡} Y) \neq \emptyset$
44	35 43	eqnetrd	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to (J fLim f) \cap Y \neq \emptyset$
45		ndisj	$⊢ (J fLim f) \cap Y \neq \emptyset \leftrightarrow \exists x (x \in (J fLim f) \land x \in Y)$
46	44 45	sylib	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to \exists x (x \in (J fLim f) \land x \in Y)$
47		mopick	$⊢ (\exists^{*} x x \in (J fLim f) \land \exists x (x \in (J fLim f) \land x \in Y)) \to (x \in (J fLim f) \to x \in Y)$
48	23 46 47	syl2anc	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to (x \in (J fLim f) \to x \in Y)$
49	19 48	mpd	$⊢ ((D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \land (f \in Fil (X) \land (Y \in f \land x \in (J fLim f)))) \to x \in Y$
50	49	rexlimdvaa	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to (\exists f \in Fil (X) (Y \in f \land x \in (J fLim f)) \to x \in Y)$
51	18 50	sylbid	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to (x \in cls (J) (Y) \to x \in Y)$
52	51	ssrdv	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to cls (J) (Y) \subseteq Y$
53	1	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
54	3 53	syl	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to J \in Top$
55	1	mopnuni	$⊢ D \in ∞Met (X) \to X = ⋃ J$
56	3 55	syl	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to X = ⋃ J$
57	16 56	sseqtrd	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to Y \subseteq ⋃ J$
58		eqid	$⊢ ⋃ J = ⋃ J$
59	58	iscld4	$⊢ (J \in Top \land Y \subseteq ⋃ J) \to (Y \in Clsd (J) \leftrightarrow cls (J) (Y) \subseteq Y)$
60	54 57 59	syl2anc	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to (Y \in Clsd (J) \leftrightarrow cls (J) (Y) \subseteq Y)$
61	52 60	mpbird	$⊢ (D \in Met (X) \land {D ↾}_{(Y \times Y)} \in CMet (Y)) \to Y \in Clsd (J)$

Metamath Proof Explorer

Theorem metsscmetcld

Proof