Description: Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | o1add2.1 | |
|
lo1mptrcl.3 | |
||
Assertion | lo1mptrcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | o1add2.1 | |
|
2 | lo1mptrcl.3 | |
|
3 | lo1f | |
|
4 | 2 3 | syl | |
5 | 1 | ralrimiva | |
6 | dmmptg | |
|
7 | 5 6 | syl | |
8 | 7 | feq2d | |
9 | 4 8 | mpbid | |
10 | 9 | fvmptelrn | |