Metamath Proof Explorer

Theorem elo1mpt

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

Ref Expression
Hypotheses elo1mpt.1 ⊢ φ → A ⊆ ℝ
elo1mpt.2 ⊢ φ ∧ x ∈ A → B ∈ ℂ
Assertion elo1mpt ⊢ φ → x ∈ A ⟼ B ∈ 𝑂⁡1 ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → B ≤ m

Proof

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