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 ‘ 𝐵 ) ≤ 𝑚 ) ) ) |
| 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 ‘ 𝐵 ) ≤ 𝑚 ) ) ) |