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 ffvelrnda ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℝ* )
47 44 45 46 syl2anc ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑥 < ( 𝐹𝑘 ) ) → ( 𝐹𝑘 ) ∈ ℝ* )
48 simpr ( ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ 𝑗𝑍 ) ∧ 𝑘 ∈ ( ℤ𝑗 ) ) ∧ 𝑥 < ( 𝐹𝑘 ) ) → 𝑥 < ( 𝐹𝑘 ) )
49 5 3ad2ant1 ( ( 𝜑𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) → 𝐹 : 𝑍 ⟶ ℝ* )
50 49 32 ffvelrnd ( ( 𝜑𝑗𝑍𝑘 ∈ ( ℤ𝑗 ) ) → ( 𝐹𝑘 ) ∈ ℝ* )
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 ralimda ( ( ( ( 𝜑𝑥 ∈ ℝ ) ∧ ( 𝑥 (,] +∞ ) ⊆ 𝑢 ) ∧ 𝑗𝑍 ) → ( ∀ 𝑘 ∈ ( ℤ𝑗 ) 𝑥 < ( 𝐹𝑘 ) → ∀ 𝑘 ∈ ( ℤ𝑗 ) ( 𝑘 ∈ 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 ( 𝜑𝐹 ~~>* +∞ )