Metamath Proof Explorer


Theorem lo1f

Description: An eventually upper bounded function is a function. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion lo1f ( 𝐹 ∈ ≤𝑂(1) → 𝐹 : dom 𝐹 ⟶ ℝ )

Proof

Step Hyp Ref Expression
1 ello1 ( 𝐹 ∈ ≤𝑂(1) ↔ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ∧ ∃ 𝑥 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑦 ∈ ( dom 𝐹 ∩ ( 𝑥 [,) +∞ ) ) ( 𝐹𝑦 ) ≤ 𝑚 ) )
2 1 simplbi ( 𝐹 ∈ ≤𝑂(1) → 𝐹 ∈ ( ℝ ↑pm ℝ ) )
3 reex ℝ ∈ V
4 3 3 elpm2 ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℝ ∧ dom 𝐹 ⊆ ℝ ) )
5 4 simplbi ( 𝐹 ∈ ( ℝ ↑pm ℝ ) → 𝐹 : dom 𝐹 ⟶ ℝ )
6 2 5 syl ( 𝐹 ∈ ≤𝑂(1) → 𝐹 : dom 𝐹 ⟶ ℝ )