Theorem lo1const

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

	Ref	Expression
Assertion	lo1const	|- ( ( A C_ RR /\ B e. RR ) -> ( x e. A |-> B ) e. <_O(1) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A C_ RR /\ B e. RR ) -> A C_ RR )
2		simplr	|- ( ( ( A C_ RR /\ B e. RR ) /\ x e. A ) -> B e. RR )
3		simpr	|- ( ( A C_ RR /\ B e. RR ) -> B e. RR )
4		leid	|- ( B e. RR -> B <_ B )
5	4	ad2antlr	|- ( ( ( A C_ RR /\ B e. RR ) /\ ( x e. A /\ B <_ x ) ) -> B <_ B )
6	1 2 3 3 5	ello1d	|- ( ( A C_ RR /\ B e. RR ) -> ( x e. A |-> B ) e. <_O(1) )