| 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 |  | xlimmnfvlem2.f | . . . . 5
⊢ (𝜑 → 𝐹:𝑍⟶ℝ*) | 
| 7 |  | xlimmnfvlem2.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 |  | mnfxr 11318 | . . . . 5
⊢ -∞
∈ ℝ* | 
| 13 | 12 | a1i 11 | . . . 4
⊢ (𝜑 → -∞ ∈
ℝ*) | 
| 14 |  | mnfnei 23229 | . . . . . . . 8
⊢ ((𝑢 ∈ (ordTop‘ ≤ )
∧ -∞ ∈ 𝑢)
→ ∃𝑥 ∈
ℝ (-∞[,)𝑥)
⊆ 𝑢) | 
| 15 | 14 | adantll 714 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ (ordTop‘ ≤ )) ∧ -∞
∈ 𝑢) →
∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝑢) | 
| 16 |  | xlimmnfvlem2.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 |  | xlimmnfvlem2.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 | 12 | a1i 11 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → -∞ ∈
ℝ*) | 
| 39 |  | simp-4r 784 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → 𝑥 ∈ ℝ) | 
| 40 |  | rexr 11307 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ*) | 
| 41 | 39, 40 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → 𝑥 ∈ ℝ*) | 
| 42 |  | simp-4l 783 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → 𝜑) | 
| 43 | 29 | ad4ant23 753 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → 𝑘 ∈ 𝑍) | 
| 44 | 6 | ffvelcdmda 7104 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) ∈
ℝ*) | 
| 45 | 42, 43, 44 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → (𝐹‘𝑘) ∈
ℝ*) | 
| 46 | 45 | mnfled 13178 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → -∞ ≤ (𝐹‘𝑘)) | 
| 47 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → (𝐹‘𝑘) < 𝑥) | 
| 48 | 38, 41, 45, 46, 47 | elicod 13437 | . . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → (𝐹‘𝑘) ∈ (-∞[,)𝑥)) | 
| 49 | 48 | adantl3r 750 | . . . . . . . . . . . . . . . . . 18
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(-∞[,)𝑥) ⊆
𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → (𝐹‘𝑘) ∈ (-∞[,)𝑥)) | 
| 50 | 37, 49 | sseldd 3984 | . . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(-∞[,)𝑥) ⊆
𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → (𝐹‘𝑘) ∈ 𝑢) | 
| 51 | 35, 50 | jca 511 | . . . . . . . . . . . . . . . 16
⊢
((((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(-∞[,)𝑥) ⊆
𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) ∧ (𝐹‘𝑘) < 𝑥) → (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) | 
| 52 | 51 | ex 412 | . . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ) ∧
(-∞[,)𝑥) ⊆
𝑢) ∧ 𝑗 ∈ 𝑍) ∧ 𝑘 ∈ (ℤ≥‘𝑗)) → ((𝐹‘𝑘) < 𝑥 → (𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 53 | 28, 52 | ralimdaa 3260 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (-∞[,)𝑥) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 54 | 53 | adantrr 717 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (-∞[,)𝑥) ⊆ 𝑢) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥)) → (∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥 → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 55 | 21, 54 | mpd 15 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (-∞[,)𝑥) ⊆ 𝑢) ∧ (𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥)) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) | 
| 56 | 55 | 3impb 1115 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (-∞[,)𝑥) ⊆ 𝑢) ∧ 𝑗 ∈ 𝑍 ∧ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥) → ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) | 
| 57 |  | xlimmnfvlem2.g | . . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑥 ∈ ℝ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥) | 
| 58 | 57 | r19.21bi 3251 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥) | 
| 59 | 58 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (-∞[,)𝑥) ⊆ 𝑢) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) < 𝑥) | 
| 60 | 20, 56, 59 | reximdd 45153 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (-∞[,)𝑥) ⊆ 𝑢) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) | 
| 61 |  | xlimmnfvlem2.m | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈ ℤ) | 
| 62 | 7 | rexuz3 15387 | . . . . . . . . . . . 12
⊢ (𝑀 ∈ ℤ →
(∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 63 | 61, 62 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 64 | 63 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (-∞[,)𝑥) ⊆ 𝑢) → (∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢) ↔ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 65 | 60, 64 | mpbid 232 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ) ∧ (-∞[,)𝑥) ⊆ 𝑢) → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) | 
| 66 | 65 | rexlimdva2 3157 | . . . . . . . 8
⊢ (𝜑 → (∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 67 | 66 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑢 ∈ (ordTop‘ ≤ )) ∧ -∞
∈ 𝑢) →
(∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 68 | 15, 67 | mpd 15 | . . . . . 6
⊢ (((𝜑 ∧ 𝑢 ∈ (ordTop‘ ≤ )) ∧ -∞
∈ 𝑢) →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)) | 
| 69 | 68 | ex 412 | . . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ (ordTop‘ ≤ )) →
(-∞ ∈ 𝑢 →
∃𝑗 ∈ ℤ
∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 70 | 69 | ralrimiva 3146 | . . . 4
⊢ (𝜑 → ∀𝑢 ∈ (ordTop‘ ≤ )(-∞ ∈
𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))) | 
| 71 | 11, 13, 70 | 3jca 1129 | . . 3
⊢ (𝜑 → (𝐹 ∈ (ℝ*
↑pm ℂ) ∧ -∞ ∈ ℝ* ∧
∀𝑢 ∈
(ordTop‘ ≤ )(-∞ ∈ 𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢)))) | 
| 72 |  | nfcv 2905 | . . . 4
⊢
Ⅎ𝑘𝐹 | 
| 73 | 72, 2 | lmbr3 45762 | . . 3
⊢ (𝜑 → (𝐹(⇝𝑡‘(ordTop‘
≤ ))-∞ ↔ (𝐹 ∈
(ℝ* ↑pm ℂ) ∧ -∞ ∈
ℝ* ∧ ∀𝑢 ∈ (ordTop‘ ≤ )(-∞ ∈
𝑢 → ∃𝑗 ∈ ℤ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑢))))) | 
| 74 | 71, 73 | mpbird 257 | . 2
⊢ (𝜑 → 𝐹(⇝𝑡‘(ordTop‘
≤ ))-∞) | 
| 75 |  | df-xlim 45834 | . . . 4
⊢ ~~>* =
(⇝𝑡‘(ordTop‘ ≤ )) | 
| 76 | 75 | breqi 5149 | . . 3
⊢ (𝐹~~>*-∞ ↔ 𝐹(⇝𝑡‘(ordTop‘
≤ ))-∞) | 
| 77 | 76 | a1i 11 | . 2
⊢ (𝜑 → (𝐹~~>*-∞ ↔ 𝐹(⇝𝑡‘(ordTop‘
≤ ))-∞)) | 
| 78 | 74, 77 | mpbird 257 | 1
⊢ (𝜑 → 𝐹~~>*-∞) |