Theorem iscms2lem4 7989

Description: Lemma for iscms2 7991. Whenever the constructed function G converges, so does the arbitrary Cauchy sequence F.

Hypotheses

Ref	Expression
iscms2lem1.1	|- G = {<.h, z>. | (h e. NN /\ z = if((F` h) e. X, (F` h), a))}
iscms2lem3.2	|- X = dom dom D

Assertion

Ref	Expression
iscms2lem4	|- ((D e. Met /\ F e. (Cau` D) /\ G(~~>m` D)x) -> F(~~>m` D)x)

Distinct variable groups:   x,a,D   h,a,z,F,x   x,G   X,a,h,x,z

Proof of Theorem iscms2lem4

Step	Hyp	Ref	Expression
1		iscms2lem3.2	. . . . 5 |- X = dom dom D
2	1	caufss 7947	. . . 4 |- ((D e. Met /\ F e. (Cau` D)) -> F (_ (CC X. X))
3	2	3adant3 801	. . 3 |- ((D e. Met /\ F e. (Cau` D) /\ G(~~>m` D)x) -> F (_ (CC X. X))
4		visset 1816	. . . . 5 |- x e. V
5	1	lmcl 7946	. . . . 5 |- ((D e. Met /\ x e. V /\ G(~~>m` D)x) -> x e. X)
6	4, 5	mp3an2 906	. . . 4 |- ((D e. Met /\ G(~~>m` D)x) -> x e. X)
7	6	3adant2 800	. . 3 |- ((D e. Met /\ F e. (Cau` D) /\ G(~~>m` D)x) -> x e. X)
8		1z 6161	. . . . . . . 8 |- 1 e. ZZ
9		nnuz 6440	. . . . . . . 8 |- NN = (ZZ>` 1)
10	1, 8, 9	iscau3 7935	. . . . . . 7 |- (D e. Met -> (F e. (Cau` D) <-> (F (_ (CC X. X) /\ A.y e. RR (0 < y -> E.m e. NN A.k e. NN (m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y))))))
11		pm3.27 323	. . . . . . 7 |- ((F (_ (CC X. X) /\ A.y e. RR (0 < y -> E.m e. NN A.k e. NN (m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y)))) -> A.y e. RR (0 < y -> E.m e. NN A.k e. NN (m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y))))
12	10, 11	syl6bi 214	. . . . . 6 |- (D e. Met -> (F e. (Cau` D) -> A.y e. RR (0 < y -> E.m e. NN A.k e. NN (m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y)))))
13	1, 8, 9	lmbr2 7926	. . . . . . . 8 |- ((D e. Met /\ x e. V) -> (G(~~>m` D)x <-> (G (_ (CC X. X) /\ x e. X /\ A.y e. RR (0 < y -> E.n e. NN A.k e. NN (n <_ k -> ((G` k) e. X /\ ((G` k)Dx) < y))))))
14	4, 13	mpan2 698	. . . . . . 7 |- (D e. Met -> (G(~~>m` D)x <-> (G (_ (CC X. X) /\ x e. X /\ A.y e. RR (0 < y -> E.n e. NN A.k e. NN (n <_ k -> ((G` k) e. X /\ ((G` k)Dx) < y))))))
15		3simp3 792	. . . . . . 7 |- ((G (_ (CC X. X) /\ x e. X /\ A.y e. RR (0 < y -> E.n e. NN A.k e. NN (n <_ k -> ((G` k) e. X /\ ((G` k)Dx) < y)))) -> A.y e. RR (0 < y -> E.n e. NN A.k e. NN (n <_ k -> ((G` k) e. X /\ ((G` k)Dx) < y))))
16	14, 15	syl6bi 214	. . . . . 6 |- (D e. Met -> (G(~~>m` D)x -> A.y e. RR (0 < y -> E.n e. NN A.k e. NN (n <_ k -> ((G` k) e. X /\ ((G` k)Dx) < y)))))
17	12, 16	anim12d 560	. . . . 5 |- (D e. Met -> ((F e. (Cau` D) /\ G(~~>m` D)x) -> (A.y e. RR (0 < y -> E.m e. NN A.k e. NN (m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y))) /\ A.y e. RR (0 < y -> E.n e. NN A.k e. NN (n <_ k -> ((G` k) e. X /\ ((G` k)Dx) < y))))))
18		iscms2lem1.1	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- G = {<.h, z>. | (h e. NN /\ z = if((F` h) e. X, (F` h), a))}
19	18	lmfexlem2 7954	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((k e. NN /\ (F` k) e. X) -> (G` k) = (F` k))
20	19	eleq1d 1543	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((k e. NN /\ (F` k) e. X) -> ((G` k) e. X <-> (F` k) e. X))
21	19	opreq1d 3981	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((k e. NN /\ (F` k) e. X) -> ((G` k)Dx) = ((F` k)Dx))
22	21	breq1d 2634	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((k e. NN /\ (F` k) e. X) -> (((G` k)Dx) < y <-> ((F` k)Dx) < y))
23	20, 22	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((k e. NN /\ (F` k) e. X) -> (((G` k) e. X /\ ((G` k)Dx) < y) <-> ((F` k) e. X /\ ((F` k)Dx) < y)))
24	23	ex 373	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (k e. NN -> ((F` k) e. X -> (((G` k) e. X /\ ((G` k)Dx) < y) <-> ((F` k) e. X /\ ((F` k)Dx) < y))))
25		3simp2 791	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y) -> (F` k) e. X)
26	24, 25	syl5 21	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (k e. NN -> (((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y) -> (((G` k) e. X /\ ((G` k)Dx) < y) <-> ((F` k) e. X /\ ((F` k)Dx) < y))))
27	26	imim2d 25	. . . . . . . . . . . . . . . . . . . . . . 23 |- (k e. NN -> ((m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y)) -> (m <_ k -> (((G` k) e. X /\ ((G` k)Dx) < y) <-> ((F` k) e. X /\ ((F` k)Dx) < y)))))
28	27	imp 350	. . . . . . . . . . . . . . . . . . . . . 22 |- ((k e. NN /\ (m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y))) -> (m <_ k -> (((G` k) e. X /\ ((G` k)Dx) < y) <-> ((F` k) e. X /\ ((F` k)Dx) < y))))
29	28	adantrd 393	. . . . . . . . . . . . . . . . . . . . 21 |- ((k e. NN /\ (m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y))) -> ((m <_ k /\ n <_ k) -> (((G` k) e. X /\ ((G` k)Dx) < y) <-> ((F` k) e. X /\ ((F` k)Dx) < y))))
30	29	pm5.74d 587	. . . . . . . . . . . . . . . . . . . 20 |- ((k e. NN /\ (m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y))) -> (((m <_ k /\ n <_ k) -> ((G` k) e. X /\ ((G` k)Dx) < y)) <-> ((m <_ k /\ n <_ k) -> ((F` k) e. X /\ ((F` k)Dx) < y))))
31		pm3.42 328	. . . . . . . . . . . . . . . . . . . 20 |- ((n <_ k -> ((G` k) e. X /\ ((G` k)Dx) < y)) -> ((m <_ k /\ n <_ k) -> ((G` k) e. X /\ ((G` k)Dx) < y)))
32	30, 31	syl5bi 208	. . . . . . . . . . . . . . . . . . 19 |- ((k e. NN /\ (m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y))) -> ((n <_ k -> ((G` k) e. X /\ ((G` k)Dx) < y)) -> ((m <_ k /\ n <_ k) -> ((F` k) e. X /\ ((F` k)Dx) < y))))
33	32	expimpd 375	. . . . . . . . . . . . . . . . . 18 |- (k e. NN -> (((m <_ k -> ((F` m) e. X /\ (F` k) e. X /\ ((F` m)D(F` k)) < y)) /\ (n <_ k -> ((G` k) e. X /\ ((G` k)Dx) < y))) -> ((m <_ k /\ n <_ k) -> ((F` k) e. X /\ ((F` k)Dx) < y))))
34	33	adantl 390	. . . . . . . . . . . . . . . . 17