Metamath Proof Explorer

Theorem elo12r

Description: Sufficient condition for elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion elo12r ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ ∧ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ A C ≤ x → F ⁡ x ≤ M → F ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 breq1 ⊢ y = C → y ≤ x ↔ C ≤ x
2 1 imbi1d ⊢ y = C → y ≤ x → F ⁡ x ≤ m ↔ C ≤ x → F ⁡ x ≤ m
3 2 ralbidv ⊢ y = C → ∀ x ∈ A y ≤ x → F ⁡ x ≤ m ↔ ∀ x ∈ A C ≤ x → F ⁡ x ≤ m
4 breq2 ⊢ m = M → F ⁡ x ≤ m ↔ F ⁡ x ≤ M
5 4 imbi2d ⊢ m = M → C ≤ x → F ⁡ x ≤ m ↔ C ≤ x → F ⁡ x ≤ M
6 5 ralbidv ⊢ m = M → ∀ x ∈ A C ≤ x → F ⁡ x ≤ m ↔ ∀ x ∈ A C ≤ x → F ⁡ x ≤ M
7 3 6 rspc2ev ⊢ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ A C ≤ x → F ⁡ x ≤ M → ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → F ⁡ x ≤ m
8 7 3expa ⊢ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ A C ≤ x → F ⁡ x ≤ M → ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → F ⁡ x ≤ m
9 8 3adant1 ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ ∧ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ A C ≤ x → F ⁡ x ≤ M → ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → F ⁡ x ≤ m
10 elo12 ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ → F ∈ 𝑂⁡1 ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → F ⁡ x ≤ m
11 10 3ad2ant1 ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ ∧ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ A C ≤ x → F ⁡ x ≤ M → F ∈ 𝑂⁡1 ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ A y ≤ x → F ⁡ x ≤ m
12 9 11 mpbird ⊢ F : A ⟶ ℂ ∧ A ⊆ ℝ ∧ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ A C ≤ x → F ⁡ x ≤ M → F ∈ 𝑂⁡1