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 φ x A B V
lo1mptrcl.3 φ x A B 𝑂1
Assertion lo1mptrcl φ x A B

Proof

Step Hyp Ref Expression
1 o1add2.1 φ x A B V
2 lo1mptrcl.3 φ x A B 𝑂1
3 lo1f x A B 𝑂1 x A B : dom x A B
4 2 3 syl φ x A B : dom x A B
5 1 ralrimiva φ x A B V
6 dmmptg x A B V dom x A B = A
7 5 6 syl φ dom x A B = A
8 7 feq2d φ x A B : dom x A B x A B : A
9 4 8 mpbid φ x A B : A
10 9 fvmptelrn φ x A B