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 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
xlimmnfvlem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
xlimmnfvlem1.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
xlimmnfvlem1.c ⊢ ( 𝜑 → 𝐹 ~~>* -∞ )
xlimmnfvlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
Assertion xlimmnfvlem1 ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 )

Proof

Step Hyp Ref Expression
1 xlimmnfvlem1.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 xlimmnfvlem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 xlimmnfvlem1.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 xlimmnfvlem1.c ⊢ ( 𝜑 → 𝐹 ~~>* -∞ )
5 xlimmnfvlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
6 icomnfordt ⊢ ( -∞ [,) 𝑋 ) ∈ ( ordTop ‘ ≤ )
7 6 a1i ⊢ ( 𝜑 → ( -∞ [,) 𝑋 ) ∈ ( ordTop ‘ ≤ ) )
8 df-xlim ⊢ ~~>* = ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) )
9 8 breqi ⊢ ( 𝐹 ~~>* -∞ ↔ 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) -∞ )
10 4 9 sylib ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) -∞ )
11 nfcv ⊢ Ⅎ 𝑘 𝐹
12 letopon ⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
13 12 a1i ⊢ ( 𝜑 → ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) )
14 11 13 lmbr3 ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( ordTop ‘ ≤ ) ) -∞ ↔ ( 𝐹 ∈ ( ℝ* ↑pm ℂ ) ∧ -∞ ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) ) )
15 10 14 mpbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( ℝ* ↑pm ℂ ) ∧ -∞ ∈ ℝ* ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
16 15 simp3d ⊢ ( 𝜑 → ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) )
17 7 16 jca ⊢ ( 𝜑 → ( ( -∞ [,) 𝑋 ) ∈ ( ordTop ‘ ≤ ) ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) )
18 15 simp2d ⊢ ( 𝜑 → -∞ ∈ ℝ* )
19 5 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
20 5 mnfltd ⊢ ( 𝜑 → -∞ < 𝑋 )
21 lbico1 ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ -∞ < 𝑋 ) → -∞ ∈ ( -∞ [,) 𝑋 ) )
22 18 19 20 21 syl3anc ⊢ ( 𝜑 → -∞ ∈ ( -∞ [,) 𝑋 ) )
23 eleq2 ⊢ ( 𝑢 = ( -∞ [,) 𝑋 ) → ( -∞ ∈ 𝑢 ↔ -∞ ∈ ( -∞ [,) 𝑋 ) ) )
24 eleq2 ⊢ ( 𝑢 = ( -∞ [,) 𝑋 ) → ( ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) )
25 24 anbi2d ⊢ ( 𝑢 = ( -∞ [,) 𝑋 ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) )
26 25 ralbidv ⊢ ( 𝑢 = ( -∞ [,) 𝑋 ) → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) )
27 26 rexbidv ⊢ ( 𝑢 = ( -∞ [,) 𝑋 ) → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) )
28 23 27 imbi12d ⊢ ( 𝑢 = ( -∞ [,) 𝑋 ) → ( ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ↔ ( -∞ ∈ ( -∞ [,) 𝑋 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) ) )
29 28 rspcva ⊢ ( ( ( -∞ [,) 𝑋 ) ∈ ( ordTop ‘ ≤ ) ∧ ∀ 𝑢 ∈ ( ordTop ‘ ≤ ) ( -∞ ∈ 𝑢 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ 𝑢 ) ) ) → ( -∞ ∈ ( -∞ [,) 𝑋 ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) )
30 17 22 29 sylc ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) )
31 nfv ⊢ Ⅎ 𝑗 𝜑
32 nfv ⊢ Ⅎ 𝑘 𝜑
33 3 ffdmd ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ* )
34 33 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
35 34 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
36 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) → 𝑋 ∈ ℝ* )
37 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) → -∞ ∈ ℝ* )
38 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) )
39 37 36 38 icoltubd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) → ( 𝐹 ‘ 𝑘 ) < 𝑋 )
40 35 36 39 xrltled ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) ) → ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 )
41 40 ex ⊢ ( 𝜑 → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 ) )
43 32 42 ralimda ⊢ ( 𝜑 → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 ) )
44 43 a1d ⊢ ( 𝜑 → ( 𝑗 ∈ ℤ → ( ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 ) ) )
45 31 44 reximdai ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( -∞ [,) 𝑋 ) ) → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 ) )
46 30 45 mpd ⊢ ( 𝜑 → ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 )
47 2 rexuz3 ⊢ ( 𝑀 ∈ ℤ → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 ) )
48 1 47 syl ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 ↔ ∃ 𝑗 ∈ ℤ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 ) )
49 46 48 mpbird ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑋 )