Metamath Proof Explorer


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 F 𝑂1 dom F

Proof

Step Hyp Ref Expression
1 elo1 F 𝑂1 F 𝑝𝑚 x m y dom F x +∞ F y m
2 1 simplbi F 𝑂1 F 𝑝𝑚
3 cnex V
4 reex V
5 3 4 elpm2 F 𝑝𝑚 F : dom F dom F
6 5 simprbi F 𝑝𝑚 dom F
7 2 6 syl F 𝑂1 dom F