Theorem caucvglem2 7111

Description: Lemma for caucvg 7116. S is a nonempty bounded subset of RR.

Hypotheses

Ref	Expression
caucvg.1	|- F:NN-->RR
caucvg.2	|- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
caucvg.3	|- S = {u e. RR | E.v e. NN A.y e. NN (v <_ y -> u < (F` y))}

Assertion

Ref	Expression
caucvglem2	|- (S (_ RR /\ S =/= (/) /\ E.x e. RR A.f e. S f <_ x)

Distinct variable groups:   x,y,z,w,u,v,f,F   x,S,z,w,f

Proof of Theorem caucvglem2

Step	Hyp	Ref	Expression
1		caucvg.3	. . 3 |- S = {u e. RR | E.v e. NN A.y e. NN (v <_ y -> u < (F` y))}
2		ssrab2 2128	. . 3 |- {u e. RR | E.v e. NN A.y e. NN (v <_ y -> u < (F` y))} (_ RR
3	1, 2	eqsstr 2088	. 2 |- S (_ RR
4		caucvg.1	. . . . 5 |- F:NN-->RR
5		axresscn 5251	. . . . 5 |- RR (_ CC
6		fss 3630	. . . . 5 |- ((F:NN-->RR /\ RR (_ CC) -> F:NN-->CC)
7	4, 5, 6	mp2an 696	. . . 4 |- F:NN-->CC
8		caucvg.2	. . . 4 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
9	7, 8	caubnd 6878	. . 3 |- E.x e. RR A.y e. NN (abs` (F` y)) < x
10		absltt 6832	. . . . . . . . . . . . . 14 |- (((F` y) e. RR /\ x e. RR) -> ((abs` (F` y)) < x <-> (-ux < (F` y) /\ (F` y) < x)))
11		pm3.26 319	. . . . . . . . . . . . . 14 |- ((-ux < (F` y) /\ (F` y) < x) -> -ux < (F` y))
12	10, 11	syl6bi 214	. . . . . . . . . . . . 13 |- (((F` y) e. RR /\ x e. RR) -> ((abs` (F` y)) < x -> -ux < (F` y)))
13	4	ffvelrni 3810	. . . . . . . . . . . . 13 |- (y e. NN -> (F` y) e. RR)
14	12, 13	sylan 448	. . . . . . . . . . . 12 |- ((y e. NN /\ x e. RR) -> ((abs` (F` y)) < x -> -ux < (F` y)))
15	14	ancoms 436	. . . . . . . . . . 11 |- ((x e. RR /\ y e. NN) -> ((abs` (F` y)) < x -> -ux < (F` y)))
16	15	a1dd 42	. . . . . . . . . 10 |- ((x e. RR /\ y e. NN) -> ((abs` (F` y)) < x -> (1 <_ y -> -ux < (F` y))))
17	16	r19.20dva 1707	. . . . . . . . 9 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> A.y e. NN (1 <_ y -> -ux < (F` y))))
18		1nn 5892	. . . . . . . . . 10 |- 1 e. NN
19	18	a1i 8	. . . . . . . . 9 |- (x e. RR -> 1 e. NN)
20	17, 19	jctild 600	. . . . . . . 8 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> (1 e. NN /\ A.y e. NN (1 <_ y -> -ux < (F` y)))))
21		breq1 2618	. . . . . . . . . . 11 |- (v = 1 -> (v <_ y <-> 1 <_ y))
22	21	imbi1d 612	. . . . . . . . . 10 |- (v = 1 -> ((v <_ y -> -ux < (F` y)) <-> (1 <_ y -> -ux < (F` y))))
23	22	ralbidv 1661	. . . . . . . . 9 |- (v = 1 -> (A.y e. NN (v <_ y -> -ux < (F` y)) <-> A.y e. NN (1 <_ y -> -ux < (F` y))))
24	23	rcla4ev 1874	. . . . . . . 8 |- ((1 e. NN /\ A.y e. NN (1 <_ y -> -ux < (F` y))) -> E.v e. NN A.y e. NN (v <_ y -> -ux < (F` y)))
25	20, 24	syl6 22	. . . . . . 7 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> E.v e. NN A.y e. NN (v <_ y -> -ux < (F` y))))
26		renegclt 5420	. . . . . . 7 |- (x e. RR -> -ux e. RR)
27	25, 26	jctild 600	. . . . . 6 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> (-ux e. RR /\ E.v e. NN A.y e. NN (v <_ y -> -ux < (F` y)))))
28	4, 8, 1	caucvglem1 7110	. . . . . 6 |- (-ux e. S <-> (-ux e. RR /\ E.v e. NN A.y e. NN (v <_ y -> -ux < (F` y))))
29	27, 28	syl6ibr 213	. . . . 5 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> -ux e. S))
30		ne0i 2283	. . . . 5 |- (-ux e. S -> S =/= (/))
31	29, 30	syl6 22	. . . 4 |- (x e. RR -> (A.y e. NN (abs` (F` y)) < x -> S =/= (/)))
32	31	r19.23aiv 1741	. . 3 |- (E.x e. RR A.y e. NN (abs` (F` y)) < x -> S =/= (/))
33	9, 32	ax-mp 7	. 2 |- S =/= (/)
34	4, 8, 1	caucvglem1 7110	. . . . . . 7 |- (f e. S <-> (f e. RR /\ E.v e. NN A.y e. NN (v <_ y -> f < (F` y))))
35		nnret 5887	. . . . . . . . . . . . . . . . . 18 |- (v e. NN -> v e. RR)
36		leidt 5514	. . . . . . . . . . . . . . . . . 18 |- (v e. RR -> v <_ v)
37	35, 36	syl 10	. . . . . . . . . . . . . . . . 17 |- (v e. NN -> v <_ v)
38		breq2 2619	. . . . . . . . . . . . . . . . . . 19 |- (y = v -> (v <_ y <-> v <_ v))
39		fveq2 3719	. . . . . . . . . . . . . . . . . . . 20 |- (y = v -> (F` y) = (F` v))
40	39	breq2d 2626	. . . . . . . . . . . . . . . . . . 19 |- (y = v -> (f < (F` y) <-> f < (F` v)))
41	38, 40	imbi12d 625	. . . . . . . . . . . . . . . . . 18 |- (y = v -> ((v <_ y -> f < (F` y)) <-> (v <_ v -> f < (F` v))))
42	41	rcla4v 1870	. . . . . . . . . . . . . . . . 17 |- (v e. NN -> (A.y e. NN (v <_ y -> f < (F` y)) -> (v <_ v -> f < (F` v))))
43	37, 42	mpid 47	. . . . . . . . . . . . . . . 16 |- (v e. NN -> (A.y e. NN (v <_ y -> f < (F` y)) -> f < (F` v)))
44	43	adantr 389	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ x e. RR) -> (A.y e. NN (v <_ y -> f < (F` y)) -> f < (F` v)))
45	39	fveq2d 3723	. . . . . . . . . . . . . . . . . . 19 |- (y = v -> (abs` (F` y)) = (abs` (F` v)))
46	45	breq1d 2625	. . . . . . . . . . . . . . . . . 18 |- (y = v -> ((abs` (F` y)) < x <-> (abs` (F` v)) < x))
47	46	rcla4v 1870	. . . . . . . . . . . . . . . . 17 |- (v e. NN -> (A.y e. NN (abs` (F` y)) < x -> (abs` (F` v)) < x))
48	47	adantr 389	. . . . . . . . . . . . . . . 16 |- ((v e. NN /\ x e. RR) -> (A.y e. NN (abs` (F` y)) < x -> (abs` (F` v)) < x))
49		absltt 6832	. . . . . . . . . . . . . . . . . 18 |- (((F` v) e. RR /\ x e. RR) -> ((abs` (F` v)) < x <-> (-ux < (F` v) /\ (F` v) < x)))
50	4	ffvelrni 3810	. . . . . . . . . . . . . . . . . 18 |- (v e. NN -> (F` v) e. RR)
51	49, 50	sylan 448	. . . . . . . . . . . . . . . . 17 |- ((v e. NN /\ x e. RR) -> ((abs` (F` v)) < x <-> (-ux < (F` v) /\ (F` v) < x)))
52		pm3.27 323	. . . . . . . . . . . . . . . . 17 |- ((-ux < (F` v) /\ (F` v) < x) -> (F` v) < x)
53	51, 52	syl6bi 214	. . . . . . . . . . . . . . . 16 |- ((v e. NN /\ x e. RR) -> ((abs` (F` v)) < x -> (F` v) < x))
54	48, 53	syld 27	. . . . . . . . . . . . . . 15 |- ((v e. NN /\ x e. RR) -> (A.y e. NN (abs` (F` y)) < x -> (F` v) < x))
55	44, 54	anim12d 557	. . . . . . . . . . . . . 14 |- ((v e. NN /\ x e. RR) -> ((A.y e. NN (v <_ y -> f < (F` y)) /\ A.y e. NN (abs` (F` y)) < x) -> (f < (F` v) /\ (F` v) < x)))
56	55	3adant1 796	. . . . . . . . . . . . 13 |- ((f e. RR /\ v e. NN /\ x e. RR) -> ((A.y e. NN (v <_ y -> f < (F` y)) /\ A.y e. NN (abs` (F` y)) < x) -> (f < (F` v) /\ (F` v) < x)))
57		axlttrn 5487	. . . . . . . . . . . . . . 15 |- ((f e. RR /\ (F` v) e. RR /\ x e. RR) -> ((f < (F` v) /\ (F` v) < x) -> f < x))
58	57, 50	syl3an2 859	. . . . . . . . . . . . . 14 |- ((f e. RR /\ v e. NN /\ x e. RR) -> ((f < (F` v) /\ (F` v) < x) -> f < x))
59		ltlet 5503	. . . . . . . . . . . . . . 15 |- ((f e. RR /\ x e. RR) -> (f < x -> f <_ x))
60	59	3adant2 797	. . . . . . . . . . . . . 14 |- ((f e. RR /\ v e. NN /\ x e. RR) -> (f < x -> f <_ x))
61	58, 60	syld 27	. . . . . . . . . . . . 13 |- ((f e. RR /\ v e. NN /\ x e. RR) -> ((f < (F` v) /\ (F` v) < x) -> f <_ x))
62	56, 61	syld 27	. . . . . . . . . . . 12 |- ((f e. RR /\ v e. NN /\ x e. RR) -> ((A.y e. NN (