Metamath Proof Explorer


Theorem o1bdd

Description: The defining property of an eventually bounded function. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion o1bdd ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 ∈ 𝑂(1) )
2 simpr ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐹 : 𝐴 ⟶ ℂ )
3 fdm ( 𝐹 : 𝐴 ⟶ ℂ → dom 𝐹 = 𝐴 )
4 3 adantl ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → dom 𝐹 = 𝐴 )
5 o1dm ( 𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ )
6 5 adantr ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → dom 𝐹 ⊆ ℝ )
7 4 6 eqsstrrd ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → 𝐴 ⊆ ℝ )
8 elo12 ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ) )
9 2 7 8 syl2anc ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ( 𝐹 ∈ 𝑂(1) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) ) )
10 1 9 mpbid ( ( 𝐹 ∈ 𝑂(1) ∧ 𝐹 : 𝐴 ⟶ ℂ ) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦𝐴 ( 𝑥𝑦 → ( abs ‘ ( 𝐹𝑦 ) ) ≤ 𝑚 ) )