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 ⊢ Ⅎ 𝑘 𝜑
xlimpnfvlem2.j ⊢ Ⅎ 𝑗 𝜑
xlimpnfvlem2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
xlimpnfvlem2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
xlimpnfvlem2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
xlimpnfvlem2.g ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )
Assertion xlimpnfvlem2 ( 𝜑 → 𝐹 ~~>* +∞ )

Proof

Step Hyp Ref Expression
1 xlimpnfvlem2.k ⊢ Ⅎ 𝑘 𝜑
2 xlimpnfvlem2.j ⊢ Ⅎ 𝑗 𝜑
3 xlimpnfvlem2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 xlimpnfvlem2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 xlimpnfvlem2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
6 xlimpnfvlem2.g ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )
7 letopon ⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
8 7 a1i ⊢ ( 𝜑 → ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) )
9 8 elfvexd ⊢ ( 𝜑 → ℝ* ∈ V )
10 cnex ⊢ ℂ ∈ V
11 10 a1i ⊢ ( 𝜑 → ℂ ∈ V )
12 4 uzsscn2 ⊢ 𝑍 ⊆ ℂ
13 12 a1i ⊢ ( 𝜑 → 𝑍 ⊆ ℂ )
14 elpm2r ⊢ ( ( ( ℝ* ∈ V ∧ ℂ ∈ V ) ∧ ( 𝐹 : 𝑍 ⟶ ℝ* ∧ 𝑍 ⊆ ℂ ) ) → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
15 9 11 5 13 14 syl22anc ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ* ↑pm ℂ ) )
16 pnfxr ⊢ +∞ ∈ ℝ*
17 16 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
18 pnfnei ⊢ ( ( 𝑢 ∈ ( ordTop ‘ ≤ ) ∧ +∞ ∈ 𝑢 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝑢 )
19 18 adantll ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ordTop ‘ ≤ ) ) ∧ +∞ ∈ 𝑢 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝑢 )
20 nfv ⊢ Ⅎ 𝑗 𝑥 ∈ ℝ
21 2 20 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ ℝ )
22 nfv ⊢ Ⅎ 𝑗 ( 𝑥 (,] +∞ ) ⊆ 𝑢
23 21 22 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 )
24 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )
25 nfv ⊢ Ⅎ 𝑘 𝑥 ∈ ℝ
26 1 25 nfan ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑥 ∈ ℝ )
27 nfv ⊢ Ⅎ 𝑘 ( 𝑥 (,] +∞ ) ⊆ 𝑢
28 26 27 nfan ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 )
29 nfv ⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
30 28 29 nfan ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 )
31 4 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
32 31 3adant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ 𝑍 )
33 5 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝑍 )
34 33 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → dom 𝐹 = 𝑍 )
35 32 34 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑘 ∈ dom 𝐹 )
36 35 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → 𝑘 ∈ dom 𝐹 )
37 36 adantl4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → 𝑘 ∈ dom 𝐹 )
38 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → ( 𝑥 (,] +∞ ) ⊆ 𝑢 )
39 38 adantl4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → ( 𝑥 (,] +∞ ) ⊆ 𝑢 )
40 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → 𝑥 ∈ ℝ )
41 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
42 40 41 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → 𝑥 ∈ ℝ* )
43 16 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → +∞ ∈ ℝ* )
44 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → 𝜑 )
45 31 ad4ant23 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → 𝑘 ∈ 𝑍 )
46 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
47 44 45 46 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
48 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → 𝑥 < ( 𝐹 ‘ 𝑘 ) )
49 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
50 49 32 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
51 50 pnfged ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ +∞ )
52 51 ad5ant134 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ +∞ )
53 42 43 47 48 52 eliocd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 (,] +∞ ) )
54 53 adantl3r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑥 (,] +∞ ) )
55 39 54 sseldd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 )
56 37 55 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
57 56 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( 𝑥 < ( 𝐹 ‘ 𝑘 ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
58 30 57 ralimdaa ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
59 58 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
60 24 59 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
61 60 3impb ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
62 6 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 < ( 𝐹 ‘ 𝑘 ) )
64 23 61 63 reximdd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
65 4 rexuz3 ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
66 3 65 syl ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
67 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
68 64 67 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
69 68 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
70 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ordTop ‘ ≤ ) ) ∧ +∞ ∈ 𝑢 ) → ( ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
71 19 70 mpd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ordTop ‘ ≤ ) ) ∧ +∞ ∈ 𝑢 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
72 71 ex ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ordTop ‘ ≤ ) ) → ( +∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
73 72 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
74 15 17 73 3jca ⊢ ( 𝜑 → ( 𝐹 ∈ ( ℝ* ↑pm ℂ ) ∧ +∞ ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
75 nfcv ⊢ Ⅎ 𝑘 𝐹
76 75 8 lmbr3 ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) +∞ ↔ ( 𝐹 ∈ ( ℝ* ↑pm ℂ ) ∧ +∞ ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
77 74 76 mpbird ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) +∞ )
78 df-xlim ⊢ ~~>* = ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) )
79 78 breqi ⊢ ( 𝐹 ~~>* +∞ ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) +∞ )
80 79 a1i ⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) +∞ ) )
81 77 80 mpbird ⊢ ( 𝜑 → 𝐹 ~~>* +∞ )