Metamath Proof Explorer

Theorem elbigofrcl

Description: Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020)

Ref Expression
Assertion elbigofrcl ⊢ F ∈ O ⁡ G → G ∈ ℝ ↑ 𝑝𝑚 ℝ

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ F ∈ O ⁡ G → G ∈ dom ⁡ O
2 df-bigo ⊢ O = g ∈ ℝ ↑ 𝑝𝑚 ℝ ⟼ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y
3 2 dmeqi ⊢ dom ⁡ O = dom ⁡ g ∈ ℝ ↑ 𝑝𝑚 ℝ ⟼ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y
4 dmmptg ⊢ ∀ g ∈ ℝ ↑ 𝑝𝑚 ℝ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y ∈ V → dom ⁡ g ∈ ℝ ↑ 𝑝𝑚 ℝ ⟼ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y = ℝ ↑ 𝑝𝑚 ℝ
5 ovex ⊢ ℝ ↑ 𝑝𝑚 ℝ ∈ V
6 5 rabex ⊢ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y ∈ V
7 6 a1i ⊢ g ∈ ℝ ↑ 𝑝𝑚 ℝ → f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y ∈ V
8 4 7 mprg ⊢ dom ⁡ g ∈ ℝ ↑ 𝑝𝑚 ℝ ⟼ f ∈ ℝ ↑ 𝑝𝑚 ℝ | ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ f ∩ x +∞ f ⁡ y ≤ m ⁢ g ⁡ y = ℝ ↑ 𝑝𝑚 ℝ
9 3 8 eqtri ⊢ dom ⁡ O = ℝ ↑ 𝑝𝑚 ℝ
10 1 9 eleqtrdi ⊢ F ∈ O ⁡ G → G ∈ ℝ ↑ 𝑝𝑚 ℝ