Theorem elo12r

Description: Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	elo12r	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 ) ) → 𝐹 ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		breq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 ≤ 𝑥 ↔ 𝐶 ≤ 𝑥 ) )
2	1	imbi1d	⊢ ( 𝑦 = 𝐶 → ( ( 𝑦 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ↔ ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ) )
3	2	ralbidv	⊢ ( 𝑦 = 𝐶 → ( ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ) )
4		breq2	⊢ ( 𝑚 = 𝑀 → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ↔ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 ) )
5	4	imbi2d	⊢ ( 𝑚 = 𝑀 → ( ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ↔ ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 ) ) )
6	5	ralbidv	⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 ) ) )
7	3 6	rspc2ev	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) )
8	7	3expa	⊢ ( ( ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) )
9	8	3adant1	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 ) ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) )
10		elo12	⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ) )
11	10	3ad2ant1	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 ) ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑥 ∈ 𝐴 ( 𝑦 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑚 ) ) )
12	9 11	mpbird	⊢ ( ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐶 ≤ 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 ) ) → 𝐹 ∈ 𝑂(1) )