Metamath Proof Explorer


Theorem rlimdmo1

Description: A convergent function is eventually bounded. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Assertion rlimdmo1 ( 𝐹 ∈ dom ⇝𝑟𝐹 ∈ 𝑂(1) )

Proof

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) )