Metamath Proof Explorer

Theorem xlimpnfvlem1

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

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

Proof

Step Hyp Ref Expression
1 xlimpnfvlem1.m 
 |-  ( ph -> M e. ZZ )
2 xlimpnfvlem1.z 
 |-  Z = ( ZZ>= ` M )
3 xlimpnfvlem1.f 
 |-  ( ph -> F : Z --> RR* )
4 xlimpnfvlem1.c 
 |-  ( ph -> F ~~>* +oo )
5 xlimpnfvlem1.x 
 |-  ( ph -> X e. RR )
6 iocpnfordt 
 |-  ( X (,] +oo ) e. ( ordTop ` <_ )
7 6 a1i 
 |-  ( ph -> ( X (,] +oo ) 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 -> ( ( X (,] +oo ) 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 5 rexrd 
 |-  ( ph -> X e. RR* )
19 15 simp2d 
 |-  ( ph -> +oo e. RR* )
20 5 ltpnfd 
 |-  ( ph -> X < +oo )
21 ubioc1 
 |-  ( ( X e. RR* /\ +oo e. RR* /\ X < +oo ) -> +oo e. ( X (,] +oo ) )
22 18 19 20 21 syl3anc 
 |-  ( ph -> +oo e. ( X (,] +oo ) )
23 eleq2 
 |-  ( u = ( X (,] +oo ) -> ( +oo e. u <-> +oo e. ( X (,] +oo ) ) )
24 eleq2 
 |-  ( u = ( X (,] +oo ) -> ( ( F ` k ) e. u <-> ( F ` k ) e. ( X (,] +oo ) ) )
25 24 anbi2d 
 |-  ( u = ( X (,] +oo ) -> ( ( k e. dom F /\ ( F ` k ) e. u ) <-> ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) ) )
26 25 ralbidv 
 |-  ( u = ( X (,] +oo ) -> ( 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. ( X (,] +oo ) ) ) )
27 26 rexbidv 
 |-  ( u = ( X (,] +oo ) -> ( 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. ( X (,] +oo ) ) ) )
28 23 27 imbi12d 
 |-  ( u = ( X (,] +oo ) -> ( ( +oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) <-> ( +oo e. ( X (,] +oo ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) ) ) )
29 28 rspcva 
 |-  ( ( ( X (,] +oo ) 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. ( X (,] +oo ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) ) )
30 17 22 29 sylc 
 |-  ( ph -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) )
31 nfv 
 |-  F/ j ph
32 nfv 
 |-  F/ k ph
33 18 adantr 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) ) -> X e. RR* )
34 3 ffdmd 
 |-  ( ph -> F : dom F --> RR* )
35 34 ffvelcdmda 
 |-  ( ( ph /\ k e. dom F ) -> ( F ` k ) e. RR* )
36 35 adantrr 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) ) -> ( F ` k ) e. RR* )
37 19 adantr 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) ) -> +oo e. RR* )
38 simprr 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) ) -> ( F ` k ) e. ( X (,] +oo ) )
39 33 37 38 iocgtlbd 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) ) -> X < ( F ` k ) )
40 33 36 39 xrltled 
 |-  ( ( ph /\ ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) ) -> X <_ ( F ` k ) )
41 40 ex 
 |-  ( ph -> ( ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) -> X <_ ( F ` k ) ) )
42 41 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` j ) ) -> ( ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) -> X <_ ( F ` k ) ) )
43 32 42 ralimdaa 
 |-  ( ph -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) -> A. k e. ( ZZ>= ` j ) X <_ ( F ` k ) ) )
44 43 a1d 
 |-  ( ph -> ( j e. ZZ -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) -> A. k e. ( ZZ>= ` j ) X <_ ( F ` k ) ) ) )
45 31 44 reximdai 
 |-  ( ph -> ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. ( X (,] +oo ) ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) X <_ ( F ` k ) ) )
46 30 45 mpd 
 |-  ( ph -> E. j e. ZZ A. k e. ( ZZ>= ` j ) X <_ ( F ` k ) )
47 2 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) X <_ ( F ` k ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) X <_ ( F ` k ) ) )
48 1 47 syl 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) X <_ ( F ` k ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) X <_ ( F ` k ) ) )
49 46 48 mpbird 
 |-  ( ph -> E. j e. Z A. k e. ( ZZ>= ` j ) X <_ ( F ` k ) )