Step |
Hyp |
Ref |
Expression |
1 |
|
lmxrge0.j |
|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
2 |
|
lmxrge0.6 |
|- ( ph -> F : NN --> ( 0 [,] +oo ) ) |
3 |
|
lmxrge0.7 |
|- ( ( ph /\ k e. NN ) -> ( F ` k ) = A ) |
4 |
|
eqid |
|- ( RR*s |`s ( 0 [,] +oo ) ) = ( RR*s |`s ( 0 [,] +oo ) ) |
5 |
|
xrstopn |
|- ( ordTop ` <_ ) = ( TopOpen ` RR*s ) |
6 |
4 5
|
resstopn |
|- ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) ) |
7 |
1 6
|
eqtr4i |
|- J = ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) |
8 |
|
letopon |
|- ( ordTop ` <_ ) e. ( TopOn ` RR* ) |
9 |
|
iccssxr |
|- ( 0 [,] +oo ) C_ RR* |
10 |
|
resttopon |
|- ( ( ( ordTop ` <_ ) e. ( TopOn ` RR* ) /\ ( 0 [,] +oo ) C_ RR* ) -> ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) ) ) |
11 |
8 9 10
|
mp2an |
|- ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) e. ( TopOn ` ( 0 [,] +oo ) ) |
12 |
7 11
|
eqeltri |
|- J e. ( TopOn ` ( 0 [,] +oo ) ) |
13 |
12
|
a1i |
|- ( ph -> J e. ( TopOn ` ( 0 [,] +oo ) ) ) |
14 |
|
nnuz |
|- NN = ( ZZ>= ` 1 ) |
15 |
|
1zzd |
|- ( ph -> 1 e. ZZ ) |
16 |
13 14 15 2 3
|
lmbrf |
|- ( ph -> ( F ( ~~>t ` J ) +oo <-> ( +oo e. ( 0 [,] +oo ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) ) ) |
17 |
|
0xr |
|- 0 e. RR* |
18 |
|
pnfxr |
|- +oo e. RR* |
19 |
|
0lepnf |
|- 0 <_ +oo |
20 |
|
ubicc2 |
|- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> +oo e. ( 0 [,] +oo ) ) |
21 |
17 18 19 20
|
mp3an |
|- +oo e. ( 0 [,] +oo ) |
22 |
21
|
biantrur |
|- ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) <-> ( +oo e. ( 0 [,] +oo ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) ) |
23 |
16 22
|
bitr4di |
|- ( ph -> ( F ( ~~>t ` J ) +oo <-> A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) ) |
24 |
|
rexr |
|- ( x e. RR -> x e. RR* ) |
25 |
18
|
a1i |
|- ( x e. RR -> +oo e. RR* ) |
26 |
|
ltpnf |
|- ( x e. RR -> x < +oo ) |
27 |
|
ubioc1 |
|- ( ( x e. RR* /\ +oo e. RR* /\ x < +oo ) -> +oo e. ( x (,] +oo ) ) |
28 |
24 25 26 27
|
syl3anc |
|- ( x e. RR -> +oo e. ( x (,] +oo ) ) |
29 |
|
0ltpnf |
|- 0 < +oo |
30 |
|
ubioc1 |
|- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 < +oo ) -> +oo e. ( 0 (,] +oo ) ) |
31 |
17 18 29 30
|
mp3an |
|- +oo e. ( 0 (,] +oo ) |
32 |
28 31
|
jctir |
|- ( x e. RR -> ( +oo e. ( x (,] +oo ) /\ +oo e. ( 0 (,] +oo ) ) ) |
33 |
|
elin |
|- ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) <-> ( +oo e. ( x (,] +oo ) /\ +oo e. ( 0 (,] +oo ) ) ) |
34 |
32 33
|
sylibr |
|- ( x e. RR -> +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) |
35 |
34
|
ad2antlr |
|- ( ( ( ph /\ x e. RR ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) -> +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) |
36 |
|
letop |
|- ( ordTop ` <_ ) e. Top |
37 |
|
ovex |
|- ( 0 [,] +oo ) e. _V |
38 |
|
iocpnfordt |
|- ( x (,] +oo ) e. ( ordTop ` <_ ) |
39 |
|
iocpnfordt |
|- ( 0 (,] +oo ) e. ( ordTop ` <_ ) |
40 |
|
inopn |
|- ( ( ( ordTop ` <_ ) e. Top /\ ( x (,] +oo ) e. ( ordTop ` <_ ) /\ ( 0 (,] +oo ) e. ( ordTop ` <_ ) ) -> ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. ( ordTop ` <_ ) ) |
41 |
36 38 39 40
|
mp3an |
|- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. ( ordTop ` <_ ) |
42 |
|
elrestr |
|- ( ( ( ordTop ` <_ ) e. Top /\ ( 0 [,] +oo ) e. _V /\ ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. ( ordTop ` <_ ) ) -> ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) i^i ( 0 [,] +oo ) ) e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) ) |
43 |
36 37 41 42
|
mp3an |
|- ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) i^i ( 0 [,] +oo ) ) e. ( ( ordTop ` <_ ) |`t ( 0 [,] +oo ) ) |
44 |
|
inss2 |
|- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) C_ ( 0 (,] +oo ) |
45 |
|
iocssicc |
|- ( 0 (,] +oo ) C_ ( 0 [,] +oo ) |
46 |
44 45
|
sstri |
|- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) C_ ( 0 [,] +oo ) |
47 |
|
sseqin2 |
|- ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) C_ ( 0 [,] +oo ) <-> ( ( 0 [,] +oo ) i^i ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) |
48 |
46 47
|
mpbi |
|- ( ( 0 [,] +oo ) i^i ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) |
49 |
|
incom |
|- ( ( 0 [,] +oo ) i^i ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) = ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) i^i ( 0 [,] +oo ) ) |
50 |
48 49
|
eqtr3i |
|- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) = ( ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) i^i ( 0 [,] +oo ) ) |
51 |
43 50 7
|
3eltr4i |
|- ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. J |
52 |
51
|
a1i |
|- ( ( ph /\ x e. RR ) -> ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) e. J ) |
53 |
|
eleq2 |
|- ( a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> ( +oo e. a <-> +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) ) |
54 |
53
|
adantl |
|- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( +oo e. a <-> +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) ) |
55 |
54
|
biimprd |
|- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> +oo e. a ) ) |
56 |
|
simp-5r |
|- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> x e. RR ) |
57 |
56
|
rexrd |
|- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> x e. RR* ) |
58 |
|
simpr |
|- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> A e. a ) |
59 |
|
simp-4r |
|- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) |
60 |
58 59
|
eleqtrd |
|- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> A e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) |
61 |
|
elin |
|- ( A e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) <-> ( A e. ( x (,] +oo ) /\ A e. ( 0 (,] +oo ) ) ) |
62 |
61
|
simplbi |
|- ( A e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> A e. ( x (,] +oo ) ) |
63 |
60 62
|
syl |
|- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> A e. ( x (,] +oo ) ) |
64 |
|
elioc1 |
|- ( ( x e. RR* /\ +oo e. RR* ) -> ( A e. ( x (,] +oo ) <-> ( A e. RR* /\ x < A /\ A <_ +oo ) ) ) |
65 |
18 64
|
mpan2 |
|- ( x e. RR* -> ( A e. ( x (,] +oo ) <-> ( A e. RR* /\ x < A /\ A <_ +oo ) ) ) |
66 |
65
|
biimpa |
|- ( ( x e. RR* /\ A e. ( x (,] +oo ) ) -> ( A e. RR* /\ x < A /\ A <_ +oo ) ) |
67 |
66
|
simp2d |
|- ( ( x e. RR* /\ A e. ( x (,] +oo ) ) -> x < A ) |
68 |
57 63 67
|
syl2anc |
|- ( ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) /\ A e. a ) -> x < A ) |
69 |
68
|
ex |
|- ( ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( A e. a -> x < A ) ) |
70 |
69
|
ralimdva |
|- ( ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) /\ l e. NN ) -> ( A. k e. ( ZZ>= ` l ) A e. a -> A. k e. ( ZZ>= ` l ) x < A ) ) |
71 |
70
|
reximdva |
|- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( E. l e. NN A. k e. ( ZZ>= ` l ) A e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) x < A ) ) |
72 |
|
fveq2 |
|- ( j = l -> ( ZZ>= ` j ) = ( ZZ>= ` l ) ) |
73 |
72
|
raleqdv |
|- ( j = l -> ( A. k e. ( ZZ>= ` j ) x < A <-> A. k e. ( ZZ>= ` l ) x < A ) ) |
74 |
73
|
cbvrexvw |
|- ( E. j e. NN A. k e. ( ZZ>= ` j ) x < A <-> E. l e. NN A. k e. ( ZZ>= ` l ) x < A ) |
75 |
71 74
|
syl6ibr |
|- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( E. l e. NN A. k e. ( ZZ>= ` l ) A e. a -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) |
76 |
55 75
|
imim12d |
|- ( ( ( ph /\ x e. RR ) /\ a = ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) ) -> ( ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) -> ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) ) |
77 |
52 76
|
rspcimdv |
|- ( ( ph /\ x e. RR ) -> ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) -> ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) ) |
78 |
77
|
imp |
|- ( ( ( ph /\ x e. RR ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) -> ( +oo e. ( ( x (,] +oo ) i^i ( 0 (,] +oo ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) |
79 |
35 78
|
mpd |
|- ( ( ( ph /\ x e. RR ) /\ A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) |
80 |
79
|
ex |
|- ( ( ph /\ x e. RR ) -> ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) -> E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) |
81 |
80
|
ralrimdva |
|- ( ph -> ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) -> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) |
82 |
|
simplll |
|- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> ph ) |
83 |
|
simpllr |
|- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> a e. J ) |
84 |
|
simpr |
|- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> +oo e. a ) |
85 |
1
|
pnfneige0 |
|- ( ( a e. J /\ +oo e. a ) -> E. x e. RR ( x (,] +oo ) C_ a ) |
86 |
83 84 85
|
syl2anc |
|- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> E. x e. RR ( x (,] +oo ) C_ a ) |
87 |
|
simplr |
|- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) |
88 |
|
r19.29r |
|- ( ( E. x e. RR ( x (,] +oo ) C_ a /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) -> E. x e. RR ( ( x (,] +oo ) C_ a /\ E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) |
89 |
|
simp-4l |
|- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ph ) |
90 |
|
uznnssnn |
|- ( l e. NN -> ( ZZ>= ` l ) C_ NN ) |
91 |
90
|
ad2antlr |
|- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( ZZ>= ` l ) C_ NN ) |
92 |
|
simpr |
|- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> k e. ( ZZ>= ` l ) ) |
93 |
91 92
|
sseldd |
|- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> k e. NN ) |
94 |
89 93
|
jca |
|- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( ph /\ k e. NN ) ) |
95 |
|
simp-4r |
|- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> x e. RR ) |
96 |
|
simpllr |
|- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( x (,] +oo ) C_ a ) |
97 |
|
simplr |
|- ( ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ x < A ) -> ( x (,] +oo ) C_ a ) |
98 |
|
simplr |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> x e. RR ) |
99 |
98
|
rexrd |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> x e. RR* ) |
100 |
2
|
ffvelrnda |
|- ( ( ph /\ k e. NN ) -> ( F ` k ) e. ( 0 [,] +oo ) ) |
101 |
3 100
|
eqeltrrd |
|- ( ( ph /\ k e. NN ) -> A e. ( 0 [,] +oo ) ) |
102 |
9 101
|
sseldi |
|- ( ( ph /\ k e. NN ) -> A e. RR* ) |
103 |
102
|
ad2antrr |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> A e. RR* ) |
104 |
|
simpr |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> x < A ) |
105 |
|
pnfge |
|- ( A e. RR* -> A <_ +oo ) |
106 |
103 105
|
syl |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> A <_ +oo ) |
107 |
65
|
biimpar |
|- ( ( x e. RR* /\ ( A e. RR* /\ x < A /\ A <_ +oo ) ) -> A e. ( x (,] +oo ) ) |
108 |
99 103 104 106 107
|
syl13anc |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ x < A ) -> A e. ( x (,] +oo ) ) |
109 |
108
|
adantlr |
|- ( ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ x < A ) -> A e. ( x (,] +oo ) ) |
110 |
97 109
|
sseldd |
|- ( ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ x < A ) -> A e. a ) |
111 |
110
|
ex |
|- ( ( ( ( ph /\ k e. NN ) /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) -> ( x < A -> A e. a ) ) |
112 |
94 95 96 111
|
syl21anc |
|- ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) /\ k e. ( ZZ>= ` l ) ) -> ( x < A -> A e. a ) ) |
113 |
112
|
ralimdva |
|- ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) /\ l e. NN ) -> ( A. k e. ( ZZ>= ` l ) x < A -> A. k e. ( ZZ>= ` l ) A e. a ) ) |
114 |
113
|
reximdva |
|- ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) -> ( E. l e. NN A. k e. ( ZZ>= ` l ) x < A -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) |
115 |
74 114
|
syl5bi |
|- ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ a ) -> ( E. j e. NN A. k e. ( ZZ>= ` j ) x < A -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) |
116 |
115
|
expimpd |
|- ( ( ph /\ x e. RR ) -> ( ( ( x (,] +oo ) C_ a /\ E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) |
117 |
116
|
rexlimdva |
|- ( ph -> ( E. x e. RR ( ( x (,] +oo ) C_ a /\ E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) |
118 |
88 117
|
syl5 |
|- ( ph -> ( ( E. x e. RR ( x (,] +oo ) C_ a /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) |
119 |
118
|
imp |
|- ( ( ph /\ ( E. x e. RR ( x (,] +oo ) C_ a /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) |
120 |
82 86 87 119
|
syl12anc |
|- ( ( ( ( ph /\ a e. J ) /\ A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) /\ +oo e. a ) -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) |
121 |
120
|
exp31 |
|- ( ( ph /\ a e. J ) -> ( A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A -> ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) ) |
122 |
121
|
ralrimdva |
|- ( ph -> ( A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A -> A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) ) ) |
123 |
81 122
|
impbid |
|- ( ph -> ( A. a e. J ( +oo e. a -> E. l e. NN A. k e. ( ZZ>= ` l ) A e. a ) <-> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) |
124 |
23 123
|
bitrd |
|- ( ph -> ( F ( ~~>t ` J ) +oo <-> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) ) |