Theorem o1lo1d

Description: A real eventually bounded function is eventually upper bounded. (Contributed by Mario Carneiro, 26-May-2016)

	Ref	Expression
Hypotheses	o1lo1.1	|- ( ( ph /\ x e. A ) -> B e. RR )
	lo1o1.1	|- ( ph -> ( x e. A |-> B ) e. O(1) )
Assertion	o1lo1d	|- ( ph -> ( x e. A |-> B ) e. <_O(1) )

Proof

Step	Hyp	Ref	Expression
1		o1lo1.1	|- ( ( ph /\ x e. A ) -> B e. RR )
2		lo1o1.1	|- ( ph -> ( x e. A |-> B ) e. O(1) )
3	1	o1lo1	|- ( ph -> ( ( x e. A |-> B ) e. O(1) <-> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) ) )
4	2 3	mpbid	|- ( ph -> ( ( x e. A |-> B ) e. <_O(1) /\ ( x e. A |-> -u B ) e. <_O(1) ) )
5	4	simpld	|- ( ph -> ( x e. A |-> B ) e. <_O(1) )