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