Metamath Proof Explorer

Theorem xlimmnfvlem1

Description: Lemma for xlimmnfv : the "only if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses xlimmnfvlem1.m 
|- ( ph -> M e. ZZ )
xlimmnfvlem1.z 
|- Z = ( ZZ>= ` M )
xlimmnfvlem1.f 
|- ( ph -> F : Z --> RR* )
xlimmnfvlem1.c 
|- ( ph -> F ~~>* -oo )
xlimmnfvlem1.x 
|- ( ph -> X e. RR )
Assertion xlimmnfvlem1 
|- ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X )

Proof

Step Hyp Ref Expression
1 xlimmnfvlem1.m 
 |-  ( ph -> M e. ZZ )
2 xlimmnfvlem1.z 
 |-  Z = ( ZZ>= ` M )
3 xlimmnfvlem1.f 
 |-  ( ph -> F : Z --> RR* )
4 xlimmnfvlem1.c 
 |-  ( ph -> F ~~>* -oo )
5 xlimmnfvlem1.x 
 |-  ( ph -> X e. RR )
6 icomnfordt 
 |-  ( -oo [,) X ) e. ( ordTop ` <_ )
7 6 a1i 
 |-  ( ph -> ( -oo [,) X ) e. ( ordTop ` <_ ) )
8 df-xlim 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
9 8 breqi 
 |-  ( F ~~>* -oo <-> F ( ~~>t ` ( ordTop ` <_ ) ) -oo )
10 4 9 sylib 
 |-  ( ph -> F ( ~~>t ` ( ordTop ` <_ ) ) -oo )
11 nfcv 
 |-  F/_ k F
12 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
13 12 a1i 
 |-  ( ph -> ( ordTop ` <_ ) e. ( TopOn ` RR* ) )
14 11 13 lmbr3 
 |-  ( ph -> ( F ( ~~>t ` ( ordTop ` <_ ) ) -oo <-> ( F e. ( RR* ^pm CC ) /\ -oo e. RR* /\ A. u e. ( ordTop ` <_ ) ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
15 10 14 mpbid 
 |-  ( ph -> ( F e. ( RR* ^pm CC ) /\ -oo e. RR* /\ A. u e. ( ordTop ` <_ ) ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
16 15 simp3d 
 |-  ( ph -> A. u e. ( ordTop ` <_ ) ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
17 7 16 jca 
 |-  ( ph -> ( ( -oo [,) X ) e. ( ordTop ` <_ ) /\ A. u e. ( ordTop ` <_ ) ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
18 15 simp2d 
 |-  ( ph -> -oo e. RR* )
19 5 rexrd 
 |-  ( ph -> X e. RR* )
20 5 mnfltd 
 |-  ( ph -> -oo < X )
21 lbico1 
 |-  ( ( -oo e. RR* /\ X e. RR* /\ -oo < X ) -> -oo e. ( -oo [,) X ) )
22 18 19 20 21 syl3anc 
 |-  ( ph -> -oo e. ( -oo [,) X ) )
23 eleq2 
 |-  ( u = ( -oo [,) X ) -> ( -oo e. u <-> -oo e. ( -oo [,) X ) ) )
24 eleq2 
 |-  ( u = ( -oo [,) X ) -> ( ( F ` k ) e. u <-> ( F ` k ) e. ( -oo [,) X ) ) )
25 24 anbi2d 
 |-  ( u = ( -oo [,) X ) -> ( ( k e. dom F /\ ( F ` k ) e. u ) <-> ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) )
26 25 ralbidv 
 |-  ( u = ( -oo [,) X ) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) )
27 26 rexbidv 
 |-  ( u = ( -oo [,) X ) -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) )
28 23 27 imbi12d 
 |-  ( u = ( -oo [,) X ) -> ( ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) <-> ( -oo e. ( -oo [,) X ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) ) )
29 28 rspcva 
 |-  ( ( ( -oo [,) X ) e. ( ordTop ` <_ ) /\ A. u e. ( ordTop ` <_ ) ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) -> ( -oo e. ( -oo [,) X ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) )
30 17 22 29 sylc 
 |-  ( ph -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) )
31 nfv 
 |-  F/ j ph
32 nfv 
 |-  F/ k ph
33 3 ffdmd 
 |-  ( ph -> F : dom F --> RR* )
34 33 ffvelcdmda 
 |-  ( ( ph /\ k e. dom F ) -> ( F ` k ) e. RR* )
35 34 adantrr 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) -> ( F ` k ) e. RR* )
36 19 adantr 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) -> X e. RR* )
37 18 adantr 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) -> -oo e. RR* )
38 simprr 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) -> ( F ` k ) e. ( -oo [,) X ) )
39 37 36 38 icoltubd 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) -> ( F ` k ) < X )
40 35 36 39 xrltled 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) ) -> ( F ` k ) <_ X )
41 40 ex 
 |-  ( ph -> ( ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) -> ( F ` k ) <_ X ) )
42 41 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` j ) ) -> ( ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) -> ( F ` k ) <_ X ) )
43 32 42 ralimdaa 
 |-  ( ph -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X ) )
44 43 a1d 
 |-  ( ph -> ( j e. ZZ -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X ) ) )
45 31 44 reximdai 
 |-  ( ph -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( -oo [,) X ) ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X ) )
46 30 45 mpd 
 |-  ( ph -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X )
47 2 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X ) )
48 1 47 syl 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X ) )
49 46 48 mpbird 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ X )