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 ⊢ φ → A ⊆ ℝ
elo1mpt.2 ⊢ φ ∧ x ∈ A → B ∈ ℂ
elo1d.3 ⊢ φ → C ∈ ℝ
Assertion elo1mpt2 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ ∃ y ∈ C +∞ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m

Proof

Step Hyp Ref Expression
1 elo1mpt.1 ⊢ φ → A ⊆ ℝ
2 elo1mpt.2 ⊢ φ ∧ x ∈ A → B ∈ ℂ
3 elo1d.3 ⊢ φ → C ∈ ℝ
4 2 lo1o12 ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ x ∈ A ⟼ B ∈ ≤𝑂⁡1
5 2 abscld ⊢ φ ∧ x ∈ A → B ∈ ℝ
6 1 5 3 ello1mpt2 ⊢ φ → x ∈ A ⟼ B ∈ ≤𝑂⁡1 ↔ ∃ y ∈ C +∞ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m
7 4 6 bitrd ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ ∃ y ∈ C +∞ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m