This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elo1

Description: Elementhood in the set of eventually bounded functions. (Contributed by Mario Carneiro, 15-Sep-2014)

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

Proof

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