Metamath Proof Explorer

Theorem xlimmnfvlem2

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

Ref Expression
Hypotheses xlimmnfvlem2.k ⊢ Ⅎ 𝑘 𝜑
xlimmnfvlem2.j ⊢ Ⅎ 𝑗 𝜑
xlimmnfvlem2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
xlimmnfvlem2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
xlimmnfvlem2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
xlimmnfvlem2.g ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 )
Assertion xlimmnfvlem2 ( 𝜑 → 𝐹 ~~>* -∞ )

Proof

Step Hyp Ref Expression
1 xlimmnfvlem2.k ⊢ Ⅎ 𝑘 𝜑
2 xlimmnfvlem2.j ⊢ Ⅎ 𝑗 𝜑
3 xlimmnfvlem2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 xlimmnfvlem2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5 xlimmnfvlem2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
6 xlimmnfvlem2.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 mnfxr ⊢ -∞ ∈ ℝ*
17 16 a1i ⊢ ( 𝜑 → -∞ ∈ ℝ* )
18 mnfnei ⊢ ( ( 𝑢 ∈ ( 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 16 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → -∞ ∈ ℝ* )
41 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → 𝑥 ∈ ℝ )
42 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
43 41 42 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → 𝑥 ∈ ℝ* )
44 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → 𝜑 )
45 31 ad4ant23 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → 𝑘 ∈ 𝑍 )
46 5 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
47 44 45 46 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
48 47 mnfled ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → -∞ ≤ ( 𝐹 ‘ 𝑘 ) )
49 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → ( 𝐹 ‘ 𝑘 ) < 𝑥 )
50 40 43 47 48 49 elicod ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑥 ) )
51 50 adantl3r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑥 ) )
52 39 51 sseldd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 )
53 37 52 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) ∧ ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
54 53 ex ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝐹 ‘ 𝑘 ) < 𝑥 → ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
55 30 54 ralimdaa ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
56 55 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 ) ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
57 24 56 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) ∧ ( 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
58 57 3impb ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) ∧ 𝑗 ∈ 𝑍 ∧ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
59 6 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 )
60 59 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) < 𝑥 )
61 23 58 60 reximdd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
62 4 rexuz3 ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
63 3 62 syl ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
64 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
65 61 64 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( -∞ [,) 𝑥 ) ⊆ 𝑢 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
66 65 rexlimdva2 ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
67 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ordTop ‘ ≤ ) ) ∧ -∞ ∈ 𝑢 ) → ( ∃ 𝑥 ∈ ℝ ( -∞ [,) 𝑥 ) ⊆ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
68 19 67 mpd ⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( ordTop ‘ ≤ ) ) ∧ -∞ ∈ 𝑢 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) )
69 68 ex ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( ordTop ‘ ≤ ) ) → ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
70 69 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
71 15 17 70 3jca ⊢ ( 𝜑 → ( 𝐹 ∈ ( ℝ* ↑pm ℂ ) ∧ -∞ ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
72 nfcv ⊢ Ⅎ 𝑘 𝐹
73 72 8 lmbr3 ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) -∞ ↔ ( 𝐹 ∈ ( ℝ* ↑pm ℂ ) ∧ -∞ ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
74 71 73 mpbird ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) -∞ )
75 df-xlim ⊢ ~~>* = ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) )
76 75 breqi ⊢ ( 𝐹 ~~>* -∞ ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) -∞ )
77 76 a1i ⊢ ( 𝜑 → ( 𝐹 ~~>* -∞ ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) -∞ ) )
78 74 77 mpbird ⊢ ( 𝜑 → 𝐹 ~~>* -∞ )