Metamath Proof Explorer

Theorem xlimpnfvlem2

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

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

Proof

Step Hyp Ref Expression
1 xlimpnfvlem2.k 
 |-  F/ k ph
2 xlimpnfvlem2.j 
 |-  F/ j ph
3 xlimpnfvlem2.m 
 |-  ( ph -> M e. ZZ )
4 xlimpnfvlem2.z 
 |-  Z = ( ZZ>= ` M )
5 xlimpnfvlem2.f 
 |-  ( ph -> F : Z --> RR* )
6 xlimpnfvlem2.g 
 |-  ( ph -> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x < ( F ` k ) )
7 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
8 7 a1i 
 |-  ( ph -> ( ordTop ` <_ ) e. ( TopOn ` RR* ) )
9 8 elfvexd 
 |-  ( ph -> RR* e. _V )
10 cnex 
 |-  CC e. _V
11 10 a1i 
 |-  ( ph -> CC e. _V )
12 4 uzsscn2 
 |-  Z C_ CC
13 12 a1i 
 |-  ( ph -> Z C_ CC )
14 elpm2r 
 |-  ( ( ( RR* e. _V /\ CC e. _V ) /\ ( F : Z --> RR* /\ Z C_ CC ) ) -> F e. ( RR* ^pm CC ) )
15 9 11 5 13 14 syl22anc 
 |-  ( ph -> F e. ( RR* ^pm CC ) )
16 pnfxr 
 |-  +oo e. RR*
17 16 a1i 
 |-  ( ph -> +oo e. RR* )
18 pnfnei 
 |-  ( ( u e. ( ordTop ` <_ ) /\ +oo e. u ) -> E. x e. RR ( x (,] +oo ) C_ u )
19 18 adantll 
 |-  ( ( ( ph /\ u e. ( ordTop ` <_ ) ) /\ +oo e. u ) -> E. x e. RR ( x (,] +oo ) C_ u )
20 nfv 
 |-  F/ j x e. RR
21 2 20 nfan 
 |-  F/ j ( ph /\ x e. RR )
22 nfv 
 |-  F/ j ( x (,] +oo ) C_ u
23 21 22 nfan 
 |-  F/ j ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u )
24 simprr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) x < ( F ` k ) ) ) -> A. k e. ( ZZ>= ` j ) x < ( F ` k ) )
25 nfv 
 |-  F/ k x e. RR
26 1 25 nfan 
 |-  F/ k ( ph /\ x e. RR )
27 nfv 
 |-  F/ k ( x (,] +oo ) C_ u
28 26 27 nfan 
 |-  F/ k ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u )
29 nfv 
 |-  F/ k j e. Z
30 28 29 nfan 
 |-  F/ k ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ j e. Z )
31 4 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
32 31 3adant1 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
33 5 fdmd 
 |-  ( ph -> dom F = Z )
34 33 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> dom F = Z )
35 32 34 eleqtrrd 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. dom F )
36 35 ad5ant134 
 |-  ( ( ( ( ( ph /\ ( x (,] +oo ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> k e. dom F )
37 36 adantl4r 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> k e. dom F )
38 simp-4r 
 |-  ( ( ( ( ( ph /\ ( x (,] +oo ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> ( x (,] +oo ) C_ u )
39 38 adantl4r 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> ( x (,] +oo ) C_ u )
40 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> x e. RR )
41 rexr 
 |-  ( x e. RR -> x e. RR* )
42 40 41 syl 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> x e. RR* )
43 16 a1i 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> +oo e. RR* )
44 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> ph )
45 31 ad4ant23 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> k e. Z )
46 5 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR* )
47 44 45 46 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> ( F ` k ) e. RR* )
48 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> x < ( F ` k ) )
49 5 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> F : Z --> RR* )
50 49 32 ffvelcdmd 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR* )
51 50 pnfged 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) <_ +oo )
52 51 ad5ant134 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> ( F ` k ) <_ +oo )
53 42 43 47 48 52 eliocd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> ( F ` k ) e. ( x (,] +oo ) )
54 53 adantl3r 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> ( F ` k ) e. ( x (,] +oo ) )
55 39 54 sseldd 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> ( F ` k ) e. u )
56 37 55 jca 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ x < ( F ` k ) ) -> ( k e. dom F /\ ( F ` k ) e. u ) )
57 56 ex 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( x < ( F ` k ) -> ( k e. dom F /\ ( F ` k ) e. u ) ) )
58 30 57 ralimdaa 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) x < ( F ` k ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
59 58 adantrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) x < ( F ` k ) ) ) -> ( A. k e. ( ZZ>= ` j ) x < ( F ` k ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
60 24 59 mpd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) x < ( F ` k ) ) ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
61 60 3impb 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) /\ j e. Z /\ A. k e. ( ZZ>= ` j ) x < ( F ` k ) ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
62 6 r19.21bi 
 |-  ( ( ph /\ x e. RR ) -> E. j e. Z A. k e. ( ZZ>= ` j ) x < ( F ` k ) )
63 62 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) -> E. j e. Z A. k e. ( ZZ>= ` j ) x < ( F ` k ) )
64 23 61 63 reximdd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
65 4 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z 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. u ) ) )
66 3 65 syl 
 |-  ( ph -> ( E. j e. Z 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. u ) ) )
67 66 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) -> ( E. j e. Z 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. u ) ) )
68 64 67 mpbid 
 |-  ( ( ( ph /\ x e. RR ) /\ ( x (,] +oo ) C_ u ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
69 68 rexlimdva2 
 |-  ( ph -> ( E. x e. RR ( x (,] +oo ) C_ u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
70 69 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ordTop ` <_ ) ) /\ +oo e. u ) -> ( E. x e. RR ( x (,] +oo ) C_ u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
71 19 70 mpd 
 |-  ( ( ( ph /\ u e. ( ordTop ` <_ ) ) /\ +oo e. u ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
72 71 ex 
 |-  ( ( ph /\ u e. ( ordTop ` <_ ) ) -> ( +oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
73 72 ralrimiva 
 |-  ( 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 ) ) )
74 15 17 73 3jca 
 |-  ( 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 ) ) ) )
75 nfcv 
 |-  F/_ k F
76 75 8 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 ) ) ) ) )
77 74 76 mpbird 
 |-  ( ph -> F ( ~~>t ` ( ordTop ` <_ ) ) +oo )
78 df-xlim 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
79 78 breqi 
 |-  ( F ~~>* +oo <-> F ( ~~>t ` ( ordTop ` <_ ) ) +oo )
80 79 a1i 
 |-  ( ph -> ( F ~~>* +oo <-> F ( ~~>t ` ( ordTop ` <_ ) ) +oo ) )
81 77 80 mpbird 
 |-  ( ph -> F ~~>* +oo )