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 ∈ B C ≤ 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 ∈ B y ≤ x → F ⁡ x ≤ m ⁢ G ⁡ x ↔ ∀ x ∈ B C ≤ 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 ∈ B C ≤ x → F ⁡ x ≤ m ⁢ G ⁡ x ↔ ∀ x ∈ B C ≤ x → F ⁡ x ≤ M ⁢ G ⁡ x
8 3 7 rspc2ev ⊢ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ B C ≤ x → F ⁡ x ≤ M ⁢ G ⁡ x → ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ B y ≤ x → F ⁡ x ≤ m ⁢ G ⁡ x
9 8 3ad2ant3 ⊢ G : A ⟶ ℝ ∧ A ⊆ ℝ ∧ F : B ⟶ ℝ ∧ B ⊆ A ∧ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ B C ≤ x → F ⁡ x ≤ M ⁢ G ⁡ x → ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ B y ≤ x → F ⁡ x ≤ m ⁢ G ⁡ x
10 elbigo2 ⊢ G : A ⟶ ℝ ∧ A ⊆ ℝ ∧ F : B ⟶ ℝ ∧ B ⊆ A → F ∈ O ⁡ G ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ B y ≤ x → F ⁡ x ≤ m ⁢ G ⁡ x
11 10 3adant3 ⊢ G : A ⟶ ℝ ∧ A ⊆ ℝ ∧ F : B ⟶ ℝ ∧ B ⊆ A ∧ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ B C ≤ x → F ⁡ x ≤ M ⁢ G ⁡ x → F ∈ O ⁡ G ↔ ∃ y ∈ ℝ ∃ m ∈ ℝ ∀ x ∈ B y ≤ x → F ⁡ x ≤ m ⁢ G ⁡ x
12 9 11 mpbird ⊢ G : A ⟶ ℝ ∧ A ⊆ ℝ ∧ F : B ⟶ ℝ ∧ B ⊆ A ∧ C ∈ ℝ ∧ M ∈ ℝ ∧ ∀ x ∈ B C ≤ x → F ⁡ x ≤ M ⁢ G ⁡ x → F ∈ O ⁡ G