Metamath Proof Explorer

Theorem bigoval

Description: Set of functions of order G(x). (Contributed by AV, 15-May-2020)

Ref Expression
Assertion bigoval ⊢ G ∈ ℝ ↑ 𝑝𝑚 ℝ → O ⁡ G = f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ G ⁡ y

Proof

Step Hyp Ref Expression
1 fveq1 ⊢ g = G → g ⁡ y = G ⁡ y
2 1 oveq2d ⊢ g = G → m ⁢ g ⁡ y = m ⁢ G ⁡ y
3 2 breq2d ⊢ g = G → f ⁡ y ≤ m ⁢ g ⁡ y ↔ f ⁡ y ≤ m ⁢ G ⁡ y
4 3 ralbidv ⊢ g = G → ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y ↔ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ G ⁡ y
5 4 2rexbidv ⊢ g = G → ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y ↔ ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ G ⁡ y
6 5 rabbidv ⊢ g = G → f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y = f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ G ⁡ y
7 df-bigo ⊢ O = g ∈ ℝ ↑ 𝑝𝑚 ℝ ⟼ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y
8 ovex ⊢ ℝ ↑ 𝑝𝑚 ℝ ∈ V
9 8 rabex ⊢ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ G ⁡ y ∈ V
10 6 7 9 fvmpt ⊢ G ∈ ℝ ↑ 𝑝𝑚 ℝ → O ⁡ G = f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ G ⁡ y