Theorem cmsss 7997

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.

Hypotheses

Ref	Expression
cmsss.1	|- X = dom dom D
cmsss.2	|- J = (Open` D)

Assertion

Ref	Expression
cmsss	|- ((D e. CMet /\ Y (_ X) -> ((D |` (Y X. Y)) e. CMet <-> Y e. (Clsd` J)))

Proof of Theorem cmsss

Step	Hyp	Ref	Expression
1		cmsss.1	. . . . . . . . 9 |- X = dom dom D
2		cmsss.2	. . . . . . . . 9 |- J = (Open` D)
3		visset 1813	. . . . . . . . 9 |- x e. V
4	1, 2, 3	metelcls 7965	. . . . . . . 8 |- ((D e. Met /\ Y (_ X) -> (x e. ((cls` J)` Y) <-> E.f(f:NN-->Y /\ f(~~>m` D)x)))
5	3	lmcau 7996	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ f(~~>m` D)x) -> f e. (Cau` D))
6	5	adantrl 394	. . . . . . . . . . . . . 14 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> f e. (Cau` D))
7		causs 7955	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ f:NN-->Y) -> (f e. (Cau` D) <-> f e. (Cau` (D |` (Y X. Y)))))
8	7	adantrr 395	. . . . . . . . . . . . . 14 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (f e. (Cau` D) <-> f e. (Cau` (D |` (Y X. Y)))))
9	6, 8	mpbid 195	. . . . . . . . . . . . 13 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> f e. (Cau` (D |` (Y X. Y))))
10		eqid 1475	. . . . . . . . . . . . . . 15 |- dom dom ( D |` (Y X. Y)) = dom dom ( D |` (Y X. Y))
11	10	cmscvg 7947	. . . . . . . . . . . . . 14 |- (((D |` (Y X. Y)) e. CMet /\ f e. (Cau` (D |` (Y X. Y)))) -> E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y)
12	11	expcom 374	. . . . . . . . . . . . 13 |- (f e. (Cau` (D |` (Y X. Y))) -> ((D |` (Y X. Y)) e. CMet -> E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y))
13	9, 12	syl 10	. . . . . . . . . . . 12 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> ((D |` (Y X. Y)) e. CMet -> E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y))
14	13	adantlr 393	. . . . . . . . . . 11 |- (((D e. Met /\ Y (_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> ((D |` (Y X. Y)) e. CMet -> E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y))
15	1	metssba2 7810	. . . . . . . . . . . . . . 15 |- ((D e. Met /\ Y (_ X) -> Y = dom dom ( D |` (Y X. Y)))
16	15	eleq2d 1541	. . . . . . . . . . . . . 14 |- ((D e. Met /\ Y (_ X) -> (y e. Y <-> y e. dom dom ( D |` (Y X. Y))))
17	16	adantr 389	. . . . . . . . . . . . 13 |- (((D e. Met /\ Y (_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (y e. Y <-> y e. dom dom ( D |` (Y X. Y))))
18		visset 1813	. . . . . . . . . . . . . . . . . 18 |- y e. V
19	3, 18	lmuni 7951	. . . . . . . . . . . . . . . . 17 |- ((D e. Met /\ f(~~>m` D)x /\ f(~~>m` D)y) -> x = y)
20		simpll 412	. . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> D e. Met)
21		simprr 415	. . . . . . . . . . . . . . . . . 18 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> f(~~>m` D)x)
22	21	adantr 389	. . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> f(~~>m` D)x)
23		lmss 7953	. . . . . . . . . . . . . . . . . . . . . 22 |- ((D e. Met /\ y e. Y /\ f:NN-->Y) -> (f(~~>m` D)y <-> f(~~>m` (D |` (Y X. Y)))y))
24	23	biimprd 154	. . . . . . . . . . . . . . . . . . . . 21 |- ((D e. Met /\ y e. Y /\ f:NN-->Y) -> (f(~~>m` (D |` (Y X. Y)))y -> f(~~>m` D)y))
25	24	3exp 832	. . . . . . . . . . . . . . . . . . . 20 |- (D e. Met -> (y e. Y -> (f:NN-->Y -> (f(~~>m` (D |` (Y X. Y)))y -> f(~~>m` D)y))))
26	25	com23 32	. . . . . . . . . . . . . . . . . . 19 |- (D e. Met -> (f:NN-->Y -> (y e. Y -> (f(~~>m` (D |` (Y X. Y)))y -> f(~~>m` D)y))))
27	26	imp43 370	. . . . . . . . . . . . . . . . . 18 |- (((D e. Met /\ f:NN-->Y) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> f(~~>m` D)y)
28	27	adantlrr 399	. . . . . . . . . . . . . . . . 17 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> f(~~>m` D)y)
29	19, 20, 22, 28	syl3anc 858	. . . . . . . . . . . . . . . 16 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> x = y)
30		eleq1a 1543	. . . . . . . . . . . . . . . . 17 |- (y e. Y -> (x = y -> x e. Y))
31	30	ad2antrl 406	. . . . . . . . . . . . . . . 16 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> (x = y -> x e. Y))
32	29, 31	mpd 26	. . . . . . . . . . . . . . 15 |- (((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) /\ (y e. Y /\ f(~~>m` (D |` (Y X. Y)))y)) -> x e. Y)
33	32	exp32 377	. . . . . . . . . . . . . 14 |- ((D e. Met /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (y e. Y -> (f(~~>m` (D |` (Y X. Y)))y -> x e. Y)))
34	33	adantlr 393	. . . . . . . . . . . . 13 |- (((D e. Met /\ Y (_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (y e. Y -> (f(~~>m` (D |` (Y X. Y)))y -> x e. Y)))
35	17, 34	sylbird 205	. . . . . . . . . . . 12 |- (((D e. Met /\ Y (_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (y e. dom dom ( D |` (Y X. Y)) -> (f(~~>m` (D |` (Y X. Y)))y -> x e. Y)))
36	35	r19.23adv 1746	. . . . . . . . . . 11 |- (((D e. Met /\ Y (_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> (E.y e. dom dom ( D |` (Y X. Y))f(~~>m` (D |` (Y X. Y)))y -> x e. Y))
37	14, 36	syld 27	. . . . . . . . . 10 |- (((D e. Met /\ Y (_ X) /\ (f:NN-->Y /\ f(~~>m` D)x)) -> ((D |` (Y X. Y)) e. CMet -> x e. Y))
38	37	ex 373	. . . . . . . . 9 |- ((D e. Met /\ Y (_ X) -> ((f:NN-->Y /\ f(~~>m` D)x) -> ((D |` (Y X. Y)) e. CMet -> x e. Y)))
39	38	19.23adv 1214	. . . . . . . 8 |- ((D e. Met /\ Y (_ X) -> (E.f(f:NN-->Y /\ f(~~>m` D)x) -> ((D |` (Y X. Y)) e. CMet -> x e. Y)))
40	4, 39	sylbid 203	. . . . . . 7 |- ((D e. Met /\ Y (_ X) -> (x e. ((cls` J)` Y) -> ((D |` (Y X. Y)) e. CMet -> x e. Y)))
41	40	com23 32	. . . . . 6 |- ((D e. Met /\ Y (_ X) -> ((D |` (Y X. Y)) e. CMet -> (x e. ((cls` J)` Y) -> x e. Y)))
42	41	imp 350	. . . . 5 |- (((D e. Met /\ Y (_ X) /\ (D |` (Y X. Y)) e. CMet) -> (x e. ((cls` J)` Y) -> x e. Y))
43	42	ssrdv 2070	. . . 4 |- (((D e. Met /\ Y (_ X) /\ (D |` (Y X. Y)) e. CMet) -> ((cls` J)` Y) (_ Y)
44		eqid 1475	. . . . . . 7 |- U.J = U.J
45	44	iscld4 7696	. . . . . 6 |- ((J e. Top /\ Y (_ U.J) -> (Y e. (Clsd` J) <-> ((cls` J)` Y) (_ Y))
46	2	opntop 7870	. . . . . . 7 |- (D e. Met -> J e. Top)
47	46	adantr 389	. . . . . 6 |- ((D e. Met /\ Y (_ X) -> J e. Top)
48	1, 2	uniopn 7861	. . . . . . . 8 |- (D e. Met -> U.J = X)
49	48	sseq2d 2089	. . . . . . 7 |- (D e. Met -> (Y (_ U.J <-> Y (_ X))
50	49	biimpar 417	. . . . . 6 |- ((D e. Met /\ Y (_ X) -> Y (_ U.J)
51	45, 47, 50	sylanc 471	. . . . 5 |- ((D e. Met /\ Y (_ X) -> (Y e. (Clsd` J) <-> ((cls` J)` Y) (_ Y))
52	51	adantr 389	. . . 4 |- (((D e. Met /\ Y (_ X) /\ (D |` (Y X. Y)) e. CMet) -> (Y e. (Clsd` J) <-> ((cls` J)` Y) (_ Y))
53	43, 52	mpbird 196	. . 3 |- (((D e. Met /\ Y (_ X)