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∈AC≤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∈Ay≤x→F⁡x≤m↔∀x∈AC≤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∈AC≤x→F⁡x≤m↔∀x∈AC≤x→F⁡x≤M
7 3 6 rspc2ev ⊢C∈ℝ∧M∈ℝ∧∀x∈AC≤x→F⁡x≤M→∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→F⁡x≤m
8 7 3expa ⊢C∈ℝ∧M∈ℝ∧∀x∈AC≤x→F⁡x≤M→∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→F⁡x≤m
9 8 3adant1 ⊢F:A⟶ℝ∧A⊆ℝ∧C∈ℝ∧M∈ℝ∧∀x∈AC≤x→F⁡x≤M→∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→F⁡x≤m
10 ello12 ⊢F:A⟶ℝ∧A⊆ℝ→F∈≤𝑂⁡1↔∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→F⁡x≤m
11 10 3ad2ant1 ⊢F:A⟶ℝ∧A⊆ℝ∧C∈ℝ∧M∈ℝ∧∀x∈AC≤x→F⁡x≤M→F∈≤𝑂⁡1↔∃y∈ℝ∃m∈ℝ∀x∈Ay≤x→F⁡x≤m
12 9 11 mpbird ⊢F:A⟶ℝ∧A⊆ℝ∧C∈ℝ∧M∈ℝ∧∀x∈AC≤x→F⁡x≤M→F∈≤𝑂⁡1