Metamath Proof Explorer


Theorem o1mptrcl

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

Ref Expression
Hypotheses o1add2.1
|- ( ( ph /\ x e. A ) -> B e. V )
o1mptrcl.3
|- ( ph -> ( x e. A |-> B ) e. O(1) )
Assertion o1mptrcl
|- ( ( ph /\ x e. A ) -> B e. CC )

Proof

Step Hyp Ref Expression
1 o1add2.1
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 o1mptrcl.3
 |-  ( ph -> ( x e. A |-> B ) e. O(1) )
3 o1f
 |-  ( ( x e. A |-> B ) e. O(1) -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC )
4 2 3 syl
 |-  ( ph -> ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC )
5 1 ralrimiva
 |-  ( ph -> A. x e. A B e. V )
6 dmmptg
 |-  ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )
7 5 6 syl
 |-  ( ph -> dom ( x e. A |-> B ) = A )
8 7 feq2d
 |-  ( ph -> ( ( x e. A |-> B ) : dom ( x e. A |-> B ) --> CC <-> ( x e. A |-> B ) : A --> CC ) )
9 4 8 mpbid
 |-  ( ph -> ( x e. A |-> B ) : A --> CC )
10 9 fvmptelrn
 |-  ( ( ph /\ x e. A ) -> B e. CC )