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

Proof

Step Hyp Ref Expression
1 xlimpnfvlem1.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 xlimpnfvlem1.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 xlimpnfvlem1.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 xlimpnfvlem1.c ⊢ ( 𝜑 → 𝐹 ~~>* +∞ )
5 xlimpnfvlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
6 iocpnfordt ⊢ ( 𝑋 (,] +∞ ) ∈ ( 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 5 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
19 15 simp2d ⊢ ( 𝜑 → +∞ ∈ ℝ* )
20 5 ltpnfd ⊢ ( 𝜑 → 𝑋 < +∞ )
21 ubioc1 ⊢ ( ( 𝑋 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑋 < +∞ ) → +∞ ∈ ( 𝑋 (,] +∞ ) )
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 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 (,] +∞ ) ) ) → 𝑋 ∈ ℝ* )
34 3 ffdmd ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ* )
35 34 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
36 35 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 (,] +∞ ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
37 19 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 (,] +∞ ) ) ) → +∞ ∈ ℝ* )
38 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 (,] +∞ ) ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 (,] +∞ ) )
39 33 37 38 iocgtlbd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ dom 𝐹 ∧ ( 𝐹 ‘ 𝑘 ) ∈ ( 𝑋 (,] +∞ ) ) ) → 𝑋 < ( 𝐹 ‘ 𝑘 ) )
40 33 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 ⊢ ( 𝜑 → ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑋 ≤ ( 𝐹 ‘ 𝑘 ) )