Theorem elbigoimp

Description: The defining property of a function of order G(x). (Contributed by AV, 18-May-2020)

	Ref	Expression
Assertion	elbigoimp	⊢ ( ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ dom 𝐺 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ dom 𝐺 ) → 𝐹 ∈ ( Ο ‘ 𝐺 ) )
2		elbigofrcl	⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) → 𝐺 ∈ ( ℝ ↑pm ℝ ) )
3		reex	⊢ ℝ ∈ V
4	3 3	elpm2	⊢ ( 𝐺 ∈ ( ℝ ↑pm ℝ ) ↔ ( 𝐺 : dom 𝐺 ⟶ ℝ ∧ dom 𝐺 ⊆ ℝ ) )
5	2 4	sylib	⊢ ( 𝐹 ∈ ( Ο ‘ 𝐺 ) → ( 𝐺 : dom 𝐺 ⟶ ℝ ∧ dom 𝐺 ⊆ ℝ ) )
6	5	3ad2ant1	⊢ ( ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ dom 𝐺 ) → ( 𝐺 : dom 𝐺 ⟶ ℝ ∧ dom 𝐺 ⊆ ℝ ) )
7		3simpc	⊢ ( ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ dom 𝐺 ) → ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ dom 𝐺 ) )
8		elbigo2	⊢ ( ( ( 𝐺 : dom 𝐺 ⟶ ℝ ∧ dom 𝐺 ⊆ ℝ ) ∧ ( 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ dom 𝐺 ) ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
9	6 7 8	syl2anc	⊢ ( ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ dom 𝐺 ) → ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) ) )
10	1 9	mpbid	⊢ ( ( 𝐹 ∈ ( Ο ‘ 𝐺 ) ∧ 𝐹 : 𝐴 ⟶ ℝ ∧ 𝐴 ⊆ dom 𝐺 ) → ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ 𝐴 ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝑚 · ( 𝐺 ‘ 𝑦 ) ) ) )