| Step | Hyp | Ref
| Expression |
| 1 | | letopon 23213 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
| 2 | 1 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (ordTop‘ ≤ )
∈ (TopOn‘ℝ*)) |
| 3 | 2 | elfvexd 6945 |
. . . . 5
⊢ (𝜑 → ℝ* ∈
V) |
| 4 | | cnex 11236 |
. . . . . 6
⊢ ℂ
∈ V |
| 5 | 4 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ∈
V) |
| 6 | | xlimpnfvlem2.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) |
| 7 | | xlimpnfvlem2.z |
. . . . . . 7
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 8 | 7 | uzsscn2 45488 |
. . . . . 6
⊢ 𝑍 ⊆
ℂ |
| 9 | 8 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑍 ⊆ ℂ) |
| 10 | | elpm2r 8885 |
. . . . 5
⊢
(((ℝ* ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝑍⟶ℝ* ∧ 𝑍 ⊆ ℂ)) → 𝐹 ∈ (ℝ*
↑pm ℂ)) |
| 11 | 3, 5, 6, 9, 10 | syl22anc 839 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℝ*
↑pm ℂ)) |
| 12 | | pnfxr 11315 |
. . . . 5
⊢ +∞
∈ ℝ* |
| 13 | 12 | a1i 11 |
. . . 4
⊢ (𝜑 → +∞ ∈
ℝ*) |
| 14 | | pnfnei 23228 |
. . . . . . . 8
⊢ ((𝑢 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ 𝑢)
→ ∃𝑥 ∈
ℝ (𝑥(,]+∞)
⊆ 𝑢) |
| 15 | 14 | adantll 714 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ (ordTop‘ ≤ )) ∧ +∞
∈ 𝑢) →
∃𝑥 ∈ ℝ
(𝑥(,]+∞) ⊆
𝑢) |
| 16 | | xlimpnfvlem2.j |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗𝜑 |
| 17 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑗 𝑥 ∈ ℝ |
| 18 | 16, 17 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(𝜑 ∧ 𝑥 ∈ ℝ) |
| 19 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(𝑥(,]+∞) ⊆ 𝑢 |
| 20 | 18, 19 | nfan 1899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) |
| 21 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))) → ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |
| 22 | | xlimpnfvlem2.k |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘𝜑 |
| 23 | | nfv 1914 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑘 𝑥 ∈ ℝ |
| 24 | 22, 23 | nfan 1899 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(𝜑 ∧ 𝑥 ∈ ℝ) |
| 25 | | nfv 1914 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘(𝑥(,]+∞) ⊆ 𝑢 |
| 26 | 24, 25 | nfan 1899 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) |
| 27 | | nfv 1914 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘 𝑗 ∈ 𝑍 |
| 28 | 26, 27 | nfan 1899 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) |
| 29 | 7 | uztrn2 12897 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
| 30 | 29 | 3adant1 1131 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ 𝑍) |
| 31 | 6 | fdmd 6746 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → dom 𝐹 = 𝑍) |
| 32 | 31 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → dom 𝐹 = 𝑍) |
| 33 | 30, 32 | eleqtrrd 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝑘 ∈ dom 𝐹) |
| 34 | 33 | ad5ant134 1369 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → 𝑘 ∈ dom 𝐹) |
| 35 | 34 | adantl4r 755 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → 𝑘 ∈ dom 𝐹) |
| 36 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → (𝑥(,]+∞) ⊆ 𝑢) |
| 37 | 36 | adantl4r 755 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → (𝑥(,]+∞) ⊆ 𝑢) |
| 38 | | simp-4r 784 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → 𝑥 ∈ ℝ) |
| 39 | | rexr 11307 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) |
| 40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → 𝑥 ∈ ℝ*) |
| 41 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → +∞ ∈
ℝ*) |
| 42 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → 𝜑) |
| 43 | 29 | ad4ant23 753 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → 𝑘 ∈ 𝑍) |
| 44 | 6 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈
ℝ*) |
| 45 | 42, 43, 44 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → (𝐹‘𝑘) ∈
ℝ*) |
| 46 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → 𝑥 < (𝐹‘𝑘)) |
| 47 | 6 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → 𝐹:𝑍⟶ℝ*) |
| 48 | 47, 30 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ∈
ℝ*) |
| 49 | 48 | pnfged 13173 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍 ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝐹‘𝑘) ≤ +∞) |
| 50 | 49 | ad5ant134 1369 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → (𝐹‘𝑘) ≤ +∞) |
| 51 | 40, 41, 45, 46, 50 | eliocd 45520 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → (𝐹‘𝑘) ∈ (𝑥(,]+∞)) |
| 52 | 51 | adantl3r 750 |
. . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → (𝐹‘𝑘) ∈ (𝑥(,]+∞)) |
| 53 | 37, 52 | sseldd 3984 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → (𝐹‘𝑘) ∈ 𝑢) |
| 54 | 35, 53 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ 𝑥 < (𝐹‘𝑘)) → (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) |
| 55 | 54 | ex 412 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → (𝑥 < (𝐹‘𝑘) → (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 56 | 28, 55 | ralimdaa 3260 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 57 | 56 | adantrr 717 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))) → (∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 58 | 21, 57 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘))) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) |
| 59 | 58 | 3impb 1115 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) |
| 60 | | xlimpnfvlem2.g |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |
| 61 | 60 | r19.21bi 3251 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |
| 62 | 61 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)𝑥 < (𝐹‘𝑘)) |
| 63 | 20, 59, 62 | reximdd 45153 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) |
| 64 | | xlimpnfvlem2.m |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 65 | 7 | rexuz3 15387 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 67 | 66 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 68 | 63, 67 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (𝑥(,]+∞) ⊆ 𝑢) → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) |
| 69 | 68 | rexlimdva2 3157 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 70 | 69 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ (ordTop‘ ≤ )) ∧ +∞
∈ 𝑢) →
(∃𝑥 ∈ ℝ
(𝑥(,]+∞) ⊆
𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 71 | 15, 70 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ (ordTop‘ ≤ )) ∧ +∞
∈ 𝑢) →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) |
| 72 | 71 | ex 412 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (ordTop‘ ≤ )) →
(+∞ ∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 73 | 72 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑢 ∈ (ordTop‘ ≤ )(+∞ ∈
𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) |
| 74 | 11, 13, 73 | 3jca 1129 |
. . 3
⊢ (𝜑 → (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ +∞ ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(+∞ ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) |
| 75 | | nfcv 2905 |
. . . 4
⊢
Ⅎ𝑘𝐹 |
| 76 | 75, 2 | lmbr3 45762 |
. . 3
⊢ (𝜑 → (𝐹(⇝𝑡‘(ordTop‘
≤ ))+∞ ↔ (𝐹 ∈
(ℝ* ↑pm ℂ) ∧ +∞ ∈
ℝ* ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(+∞ ∈
𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) |
| 77 | 74, 76 | mpbird 257 |
. 2
⊢ (𝜑 → 𝐹(⇝𝑡‘(ordTop‘
≤ ))+∞) |
| 78 | | df-xlim 45834 |
. . . 4
⊢ ~~>* =
(⇝𝑡‘(ordTop‘ ≤ )) |
| 79 | 78 | breqi 5149 |
. . 3
⊢ (𝐹~~>*+∞ ↔ 𝐹(⇝𝑡‘(ordTop‘
≤ ))+∞) |
| 80 | 79 | a1i 11 |
. 2
⊢ (𝜑 → (𝐹~~>*+∞ ↔ 𝐹(⇝𝑡‘(ordTop‘
≤ ))+∞)) |
| 81 | 77, 80 | mpbird 257 |
1
⊢ (𝜑 → 𝐹~~>*+∞) |