Theorem rlimdmo1

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

	Ref	Expression
Assertion	rlimdmo1	|- ( F e. dom ~~>r -> F e. O(1) )

Proof

Step	Hyp	Ref	Expression
1		eldmg	|- ( F e. dom ~~>r -> ( F e. dom ~~>r <-> E. x F ~~>r x ) )
2	1	ibi	|- ( F e. dom ~~>r -> E. x F ~~>r x )
3		rlimo1	|- ( F ~~>r x -> F e. O(1) )
4	3	exlimiv	|- ( E. x F ~~>r x -> F e. O(1) )
5	2 4	syl	|- ( F e. dom ~~>r -> F e. O(1) )