Metamath Proof Explorer


Theorem elo1mpt2

Description: Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 12-May-2016) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses elo1mpt.1 ( 𝜑𝐴 ⊆ ℝ )
elo1mpt.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
elo1d.3 ( 𝜑𝐶 ∈ ℝ )
Assertion elo1mpt2 ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑦𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ) )

Proof

Step Hyp Ref Expression
1 elo1mpt.1 ( 𝜑𝐴 ⊆ ℝ )
2 elo1mpt.2 ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
3 elo1d.3 ( 𝜑𝐶 ∈ ℝ )
4 2 lo1o12 ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ) )
5 2 abscld ( ( 𝜑𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
6 1 5 3 ello1mpt2 ( 𝜑 → ( ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ ≤𝑂(1) ↔ ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑦𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ) )
7 4 6 bitrd ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝑂(1) ↔ ∃ 𝑦 ∈ ( 𝐶 [,) +∞ ) ∃ 𝑚 ∈ ℝ ∀ 𝑥𝐴 ( 𝑦𝑥 → ( abs ‘ 𝐵 ) ≤ 𝑚 ) ) )