Description: An eventually upper bounded function is a function. (Contributed by Mario Carneiro, 26-May-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | lo1f | ⊢ ( 𝐹 ∈ ≤𝑂(1) → 𝐹 : dom 𝐹 ⟶ ℝ ) |
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 𝐹 ⟶ ℝ ) |