Metamath Proof Explorer

Theorem elbigo2r

Description: Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020)

Ref Expression
Assertion elbigo2r ⊢G:A⟶ℝ∧A⊆ℝ∧F:B⟶ℝ∧B⊆A∧C∈ℝ∧M∈ℝ∧∀x∈BC≤x→F⁡x≤M⁢G⁡x→F∈O⁡G

Proof

Step Hyp Ref Expression
1 breq1 ⊢y=C→y≤x↔C≤x
2 1 imbi1d ⊢y=C→y≤x→F⁡x≤m⁢G⁡x↔C≤x→F⁡x≤m⁢G⁡x
3 2 ralbidv ⊢y=C→∀x∈By≤x→F⁡x≤m⁢G⁡x↔∀x∈BC≤x→F⁡x≤m⁢G⁡x
4 oveq1 ⊢m=M→m⁢G⁡x=M⁢G⁡x
5 4 breq2d ⊢m=M→F⁡x≤m⁢G⁡x↔F⁡x≤M⁢G⁡x
6 5 imbi2d ⊢m=M→C≤x→F⁡x≤m⁢G⁡x↔C≤x→F⁡x≤M⁢G⁡x
7 6 ralbidv ⊢m=M→∀x∈BC≤x→F⁡x≤m⁢G⁡x↔∀x∈BC≤x→F⁡x≤M⁢G⁡x
8 3 7 rspc2ev ⊢C∈ℝ∧M∈ℝ∧∀x∈BC≤x→F⁡x≤M⁢G⁡x→∃y∈ℝ∃m∈ℝ∀x∈By≤x→F⁡x≤m⁢G⁡x
9 8 3ad2ant3 ⊢G:A⟶ℝ∧A⊆ℝ∧F:B⟶ℝ∧B⊆A∧C∈ℝ∧M∈ℝ∧∀x∈BC≤x→F⁡x≤M⁢G⁡x→∃y∈ℝ∃m∈ℝ∀x∈By≤x→F⁡x≤m⁢G⁡x
10 elbigo2 ⊢G:A⟶ℝ∧A⊆ℝ∧F:B⟶ℝ∧B⊆A→F∈O⁡G↔∃y∈ℝ∃m∈ℝ∀x∈By≤x→F⁡x≤m⁢G⁡x
11 10 3adant3 ⊢G:A⟶ℝ∧A⊆ℝ∧F:B⟶ℝ∧B⊆A∧C∈ℝ∧M∈ℝ∧∀x∈BC≤x→F⁡x≤M⁢G⁡x→F∈O⁡G↔∃y∈ℝ∃m∈ℝ∀x∈By≤x→F⁡x≤m⁢G⁡x
12 9 11 mpbird ⊢G:A⟶ℝ∧A⊆ℝ∧F:B⟶ℝ∧B⊆A∧C∈ℝ∧M∈ℝ∧∀x∈BC≤x→F⁡x≤M⁢G⁡x→F∈O⁡G