Metamath Proof Explorer

Theorem elbigofrcl

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

		Ref	Expression
	Assertion	elbigofrcl	$⊢ F \in O (G) \to G \in (ℝ ↑_{𝑝𝑚} ℝ)$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ F \in O (G) \to G \in dom O$
2		df-bigo	$⊢ O = (g \in (ℝ ↑_{𝑝𝑚} ℝ) ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\})$
3	2	dmeqi	$⊢ dom O = dom (g \in (ℝ ↑_{𝑝𝑚} ℝ) ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\})$
4		dmmptg	$⊢ \forall g \in (ℝ ↑_{𝑝𝑚} ℝ) \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\} \in V \to dom (g \in (ℝ ↑_{𝑝𝑚} ℝ) ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\}) = ℝ ↑_{𝑝𝑚} ℝ$
5		ovex	$⊢ ℝ ↑_{𝑝𝑚} ℝ \in V$
6	5	rabex	$⊢ \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\} \in V$
7	6	a1i	$⊢ g \in (ℝ ↑_{𝑝𝑚} ℝ) \to \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\} \in V$
8	4 7	mprg	$⊢ dom (g \in (ℝ ↑_{𝑝𝑚} ℝ) ⟼ \{f \in (ℝ ↑_{𝑝𝑚} ℝ) \| \exists x \in ℝ \exists m \in ℝ \forall y \in (dom f \cap [x, +∞)) f (y) \leq m g (y)\}) = ℝ ↑_{𝑝𝑚} ℝ$
9	3 8	eqtri	$⊢ dom O = ℝ ↑_{𝑝𝑚} ℝ$
10	1 9	eleqtrdi	$⊢ F \in O (G) \to G \in (ℝ ↑_{𝑝𝑚} ℝ)$