Description: A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | rlimdmo1 | ⊢ ( 𝐹 ∈ dom ⇝𝑟 → 𝐹 ∈ 𝑂(1) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldmg | ⊢ ( 𝐹 ∈ dom ⇝𝑟 → ( 𝐹 ∈ dom ⇝𝑟 ↔ ∃ 𝑥 𝐹 ⇝𝑟 𝑥 ) ) | |
2 | 1 | ibi | ⊢ ( 𝐹 ∈ dom ⇝𝑟 → ∃ 𝑥 𝐹 ⇝𝑟 𝑥 ) |
3 | rlimo1 | ⊢ ( 𝐹 ⇝𝑟 𝑥 → 𝐹 ∈ 𝑂(1) ) | |
4 | 3 | exlimiv | ⊢ ( ∃ 𝑥 𝐹 ⇝𝑟 𝑥 → 𝐹 ∈ 𝑂(1) ) |
5 | 2 4 | syl | ⊢ ( 𝐹 ∈ dom ⇝𝑟 → 𝐹 ∈ 𝑂(1) ) |