Theorem elbigo

Description: Properties of a function of order G(x). (Contributed by AV, 16-May-2020)

	Ref	Expression
Assertion	elbigo	⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bigoval	⊢ ( 𝐺 ∈ ( ℝ ↑pm ℝ ) → ( Ο ‘ 𝐺 ) = { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) } )
2	1	eleq2d	⊢ ( 𝐺 ∈ ( ℝ ↑pm ℝ ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) } ) )
3		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
4	3	ineq1d	⊢ ( 𝑓 = 𝐹 → ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) = ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) )
5		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
6	5	breq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
7	4 6	raleqbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
8	7	2rexbidv	⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
9	8	elrab	⊢ ( 𝐹 ∈ { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) } ↔ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )
10	2 9	bitrdi	⊢ ( 𝐺 ∈ ( ℝ ↑pm ℝ ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
11	10	pm5.32i	⊢ ( ( 𝐺 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐹 ∈ ( Ο ‘ 𝐺 ) ) ↔ ( 𝐺 ∈ ( ℝ ↑pm ℝ ) ∧ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
12		elbigofrcl	⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) → 𝐺 ∈ ( ℝ ↑pm ℝ ) )
13	12	pm4.71ri	⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ( 𝐺 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐹 ∈ ( Ο ‘ 𝐺 ) ) )
14		3anan12	⊢ ( ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( 𝐺 ∈ ( ℝ ↑pm ℝ ) ∧ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
15	11 13 14	3bitr4i	⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ 𝐺 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )