Theorem bigoval

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

	Ref	Expression
Assertion	bigoval	⊢ ( 𝐺 ∈ ( ℝ ↑pm ℝ ) → ( Ο ‘ 𝐺 ) = { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		fveq1	⊢ ( 𝑔 = 𝐺 → ( 𝑔 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
2	1	oveq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) = ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) )
3	2	breq2d	⊢ ( 𝑔 = 𝐺 → ( ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) ↔ ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
4	3	ralbidv	⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
5	4	2rexbidv	⊢ ( 𝑔 = 𝐺 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
6	5	rabbidv	⊢ ( 𝑔 = 𝐺 → { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } = { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) } )
7		df-bigo	⊢ Ο = ( 𝑔 ∈ ( ℝ ↑pm ℝ ) ↦ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝑔 ‘ 𝑦 ) ) } )
8		ovex	⊢ ( ℝ ↑pm ℝ ) ∈ V
9	8	rabex	⊢ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) } ∈ V
10	6 7 9	fvmpt	⊢ ( 𝐺 ∈ ( ℝ ↑pm ℝ ) → ( Ο ‘ 𝐺 ) = { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) } )