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 ⊢ F ∈ ≤𝑂⁡1 → F : dom ⁡ F ⟶ ℝ

Proof

Step Hyp Ref Expression
1 ello1 ⊢ F ∈ ≤𝑂⁡1 ↔ F ∈ ℝ ↑ 𝑝𝑚 ℝ ∧ ∃ x ∈ ℝ ∃ m ∈ ℝ ∀ y ∈ dom ⁡ F ∩ x +∞ F ⁡ y ≤ m
2 1 simplbi ⊢ F ∈ ≤𝑂⁡1 → F ∈ ℝ ↑ 𝑝𝑚 ℝ
3 reex ⊢ ℝ ∈ V
4 3 3 elpm2 ⊢ F ∈ ℝ ↑ 𝑝𝑚 ℝ ↔ F : dom ⁡ F ⟶ ℝ ∧ dom ⁡ F ⊆ ℝ
5 4 simplbi ⊢ F ∈ ℝ ↑ 𝑝𝑚 ℝ → F : dom ⁡ F ⟶ ℝ
6 2 5 syl ⊢ F ∈ ≤𝑂⁡1 → F : dom ⁡ F ⟶ ℝ