Metamath Proof Explorer

Theorem ello12r

Description: Sufficient condition for elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion ello12r ⊢ 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 ello12 ⊢ 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