Theorem elbigofrcl

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

	Ref	Expression
Assertion	elbigofrcl	⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) → 𝐺 ∈ ( ℝ ↑pm ℝ ) )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) → 𝐺 ∈ dom Ο )
2		df-bigo	⊢ Ο = ( 𝑔 ∈ ( ℝ ↑pm ℝ ) ↦ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } )
3	2	dmeqi	⊢ dom Ο = dom ( 𝑔 ∈ ( ℝ ↑pm ℝ ) ↦ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } )
4		dmmptg	⊢ ( ∀ 𝑔 ∈ ( ℝ ↑pm ℝ ) { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } ∈ V → dom ( 𝑔 ∈ ( ℝ ↑pm ℝ ) ↦ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } ) = ( ℝ ↑pm ℝ ) )
5		ovex	⊢ ( ℝ ↑pm ℝ ) ∈ V
6	5	rabex	⊢ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } ∈ V
7	6	a1i	⊢ ( 𝑔 ∈ ( ℝ ↑pm ℝ ) → { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } ∈ V )
8	4 7	mprg	⊢ dom ( 𝑔 ∈ ( ℝ ↑pm ℝ ) ↦ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } ) = ( ℝ ↑pm ℝ )
9	3 8	eqtri	⊢ dom Ο = ( ℝ ↑pm ℝ )
10	1 9	eleqtrdi	⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) → 𝐺 ∈ ( ℝ ↑pm ℝ ) )