Theorem caussi 7954

Description: Cauchy sequence on a metric subspace.

Assertion

Ref	Expression
caussi	|- ((D e. Met /\ F e. (Cau` (D |` (Y X. Y)))) -> F e. (Cau` D))

Proof of Theorem caussi

Step	Hyp	Ref	Expression
1		ssid 2080	. . . . . . 7 |- CC (_ CC
2		resss 3383	. . . . . . . . 9 |- (D |` (Y X. Y)) (_ D
3		dmss 3310	. . . . . . . . 9 |- ((D |` (Y X. Y)) (_ D -> dom ( D |` (Y X. Y)) (_ dom D)
4	2, 3	ax-mp 7	. . . . . . . 8 |- dom ( D |` (Y X. Y)) (_ dom D
5		dmss 3310	. . . . . . . 8 |- (dom ( D |` (Y X. Y)) (_ dom D -> dom dom ( D |` (Y X. Y)) (_ dom dom D)
6	4, 5	ax-mp 7	. . . . . . 7 |- dom dom ( D |` (Y X. Y)) (_ dom dom D
7		ssxp 3256	. . . . . . 7 |- ((CC (_ CC /\ dom dom ( D |` (Y X. Y)) (_ dom dom D) -> (CC X. dom dom ( D |` (Y X. Y))) (_ (CC X. dom dom D))
8	1, 6, 7	mp2an 697	. . . . . 6 |- (CC X. dom dom ( D |` (Y X. Y))) (_ (CC X. dom dom D)
9		sstr 2072	. . . . . 6 |- ((F (_ (CC X. dom dom ( D |` (Y X. Y))) /\ (CC X. dom dom ( D |` (Y X. Y))) (_ (CC X. dom dom D)) -> F (_ (CC X. dom dom D))
10	8, 9	mpan2 696	. . . . 5 |- (F (_ (CC X. dom dom ( D |` (Y X. Y))) -> F (_ (CC X. dom dom D))
11	10	a1i 8	. . . 4 |- (D e. Met -> (F (_ (CC X. dom dom ( D |` (Y X. Y))) -> F (_ (CC X. dom dom D)))
12	6	sseli 2065	. . . . . . . . . . . 12 |- ((F` j) e. dom dom ( D |` (Y X. Y)) -> (F` j) e. dom dom D)
13	12	3ad2ant1 800	. . . . . . . . . . 11 |- (((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x) -> (F` j) e. dom dom D)
14	13	a1i 8	. . . . . . . . . 10 |- (D e. Met -> (((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x) -> (F` j) e. dom dom D))
15	6	sseli 2065	. . . . . . . . . . . 12 |- ((F` k) e. dom dom ( D |` (Y X. Y)) -> (F` k) e. dom dom D)
16	15	3ad2ant2 801	. . . . . . . . . . 11 |- (((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x) -> (F` k) e. dom dom D)
17	16	a1i 8	. . . . . . . . . 10 |- (D e. Met -> (((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x) -> (F` k) e. dom dom D))
18		oprvalres 4033	. . . . . . . . . . . . . . . 16 |- (((F` j) e. Y /\ (F` k) e. Y) -> ((F` j)(D |` (Y X. Y))(F` k)) = ((F` j)D(F` k)))
19		eqid 1475	. . . . . . . . . . . . . . . . . . . 20 |- dom dom D = dom dom D
20	19	metssba 7809	. . . . . . . . . . . . . . . . . . 19 |- (D e. Met -> (dom dom D i^i Y) = dom dom ( D |` (Y X. Y)))
21		inss2 2231	. . . . . . . . . . . . . . . . . . . 20 |- (dom dom D i^i Y) (_ Y
22	21	a1i 8	. . . . . . . . . . . . . . . . . . 19 |- (D e. Met -> (dom dom D i^i Y) (_ Y)
23	20, 22	eqsstr3d 2096	. . . . . . . . . . . . . . . . . 18 |- (D e. Met -> dom dom ( D |` (Y X. Y)) (_ Y)
24	23	sseld 2067	. . . . . . . . . . . . . . . . 17 |- (D e. Met -> ((F` j) e. dom dom ( D |` (Y X. Y)) -> (F` j) e. Y))
25	24	imp 350	. . . . . . . . . . . . . . . 16 |- ((D e. Met /\ (F` j) e. dom dom ( D |` (Y X. Y))) -> (F` j) e. Y)
26	23	sseld 2067	. . . . . . . . . . . . . . . . 17 |- (D e. Met -> ((F` k) e. dom dom ( D |` (Y X. Y)) -> (F` k) e. Y))
27	26	imp 350	. . . . . . . . . . . . . . . 16 |- ((D e. Met /\ (F` k) e. dom dom ( D |` (Y X. Y))) -> (F` k) e. Y)
28	18, 25, 27	syl2an 454	. . . . . . . . . . . . . . 15 |- (((D e. Met /\ (F` j) e. dom dom ( D |` (Y X. Y))) /\ (D e. Met /\ (F` k) e. dom dom ( D |` (Y X. Y)))) -> ((F` j)(D |` (Y X. Y))(F` k)) = ((F` j)D(F` k)))
29	28	anandis 512	. . . . . . . . . . . . . 14 |- ((D e. Met /\ ((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)))) -> ((F` j)(D |` (Y X. Y))(F` k)) = ((F` j)D(F` k)))
30	29	breq1d 2629	. . . . . . . . . . . . 13 |- ((D e. Met /\ ((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)))) -> (((F` j)(D |` (Y X. Y))(F` k)) < x <-> ((F` j)D(F` k)) < x))
31	30	biimpd 153	. . . . . . . . . . . 12 |- ((D e. Met /\ ((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)))) -> (((F` j)(D |` (Y X. Y))(F` k)) < x -> ((F` j)D(F` k)) < x))
32	31	exp32 377	. . . . . . . . . . 11 |- (D e. Met -> ((F` j) e. dom dom ( D |` (Y X. Y)) -> ((F` k) e. dom dom ( D |` (Y X. Y)) -> (((F` j)(D |` (Y X. Y))(F` k)) < x -> ((F` j)D(F` k)) < x))))
33	32	3impd 847	. . . . . . . . . 10 |- (D e. Met -> (((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x) -> ((F` j)D(F` k)) < x))
34	14, 17, 33	3jcad 820	. . . . . . . . 9 |- (D e. Met -> (((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x) -> ((F` j) e. dom dom D /\ (F` k) e. dom dom D /\ ((F` j)D(F` k)) < x)))
35	34	imim2d 25	. . . . . . . 8 |- (D e. Met -> ((j <_ k -> ((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x)) -> (j <_ k -> ((F` j) e. dom dom D /\ (F` k) e. dom dom D /\ ((F` j)D(F` k)) < x))))
36	35	r19.20sdv 1710	. . . . . . 7 |- (D e. Met -> (A.k e. NN (j <_ k -> ((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x)) -> A.k e. NN (j <_ k -> ((F` j) e. dom dom D /\ (F` k) e. dom dom D /\ ((F` j)D(F` k)) < x))))
37	36	r19.22sdv 1738	. . . . . 6 |- (D e. Met -> (E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x)) -> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. dom dom D /\ (F` k) e. dom dom D /\ ((F` j)D(F` k)) < x))))
38	37	imim2d 25	. . . . 5 |- (D e. Met -> ((0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. dom dom ( D |` (Y X. Y)) /\ (F` k) e. dom dom ( D |` (Y X. Y)) /\ ((F` j)(D |` (Y X. Y))(F` k)) < x))) -> (0 < x -> E.j e. NN A.k e. NN (j <_ k -> ((F` j) e. dom dom D /\ (F` k) e. dom dom D /\ ((F