Metamath Proof Explorer


Theorem lo1mptrcl

Description: Reverse closure for an eventually upper bounded function. (Contributed by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses o1add2.1 φxABV
lo1mptrcl.3 φxAB𝑂1
Assertion lo1mptrcl φxAB

Proof

Step Hyp Ref Expression
1 o1add2.1 φxABV
2 lo1mptrcl.3 φxAB𝑂1
3 lo1f xAB𝑂1xAB:domxAB
4 2 3 syl φxAB:domxAB
5 1 ralrimiva φxABV
6 dmmptg xABVdomxAB=A
7 5 6 syl φdomxAB=A
8 7 feq2d φxAB:domxABxAB:A
9 4 8 mpbid φxAB:A
10 9 fvmptelrn φxAB