Theorem elo1d

Description: Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 21-Sep-2014) (Proof shortened by Mario Carneiro, 26-May-2016)

	Ref	Expression
Hypotheses	elo1mpt.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	elo1mpt.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	elo1d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	elo1d.4	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
	elo1d.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → ( abs ‘ 𝐵 ) ≤ 𝑀 )
Assertion	elo1d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		elo1mpt.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		elo1mpt.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3		elo1d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		elo1d.4	⊢ ( 𝜑 → 𝑀 ∈ ℝ )
5		elo1d.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ≤ 𝑥 ) ) → ( abs ‘ 𝐵 ) ≤ 𝑀 )
6	2	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
7	1 6 3 4 5	ello1d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) )
8	2	lo1o12	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) )
9	7 8	mpbird	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )