Theorem o1dm

Description: An eventually bounded function's domain is a subset of the reals. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	o1dm	⊢ ( 𝐹 ∈ 𝑂(1) → dom 𝐹 ⊆ ℝ )

Proof

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