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