Theorem ello1

Description: Elementhood in the set of eventually upper bounded functions. (Contributed by Mario Carneiro, 26-May-2016)

	Ref	Expression
Assertion	ello1	⊢ ( 𝐹 ∈ ≤𝑂(1) ↔ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )

Proof

Step	Hyp	Ref	Expression
1		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
2	1	ineq1d	⊢ ( 𝑓 = 𝐹 → ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) = ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) )
3		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
4	3	breq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ‘ 𝑦 ) ≤ 𝑚 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
5	2 4	raleqbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ 𝑚 ↔ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
6	5	2rexbidv	⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ 𝑚 ↔ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )
7		df-lo1	⊢ ≤𝑂(1) = { 𝑓 ∈ ( ℝ ↑pm ℝ ) ∣ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝑓 ∩ ( 𝑥 [,) +∞ ) ) ( 𝑓 ‘ 𝑦 ) ≤ 𝑚 }
8	6 7	elrab2	⊢ ( 𝐹 ∈ ≤𝑂(1) ↔ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹 ‘ 𝑦 ) ≤ 𝑚 ) )