Metamath Proof Explorer

Theorem lo1dm

Description: An eventually upper bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Assertion lo1dm ⊢ F ∈ ≤𝑂⁡1 → 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 simprbi ⊢ F ∈ ℝ ↑ 𝑝𝑚 ℝ → dom ⁡ F ⊆ ℝ
6 2 5 syl ⊢ F ∈ ≤𝑂⁡1 → dom ⁡ F ⊆ ℝ