Metamath Proof Explorer

Theorem lmxrge0

Description: Express "sequence F converges to plus infinity" (i.e. diverges), for a sequence of nonnegative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017)

Ref Expression
Hypotheses lmxrge0.j 
|- J = ( TopOpen ` ( RR*s |`s ( 0 [,] +oo ) ) )
lmxrge0.6 
|- ( ph -> F : NN --> ( 0 [,] +oo ) )
lmxrge0.7 
|- ( ( ph /\ k e. NN ) -> ( F ` k ) = A )
Assertion lmxrge0 
|- ( ph -> ( F ( ~~>t ` J ) +oo <-> A. x e. RR E. j e. NN A. k e. ( ZZ>= ` j ) x < A ) )

Proof

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 sselid 
 |-  ( ( 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 ) )