This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimmptrcl

Description: Reverse closure for a real limit. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimabs.1 
|- ( ( ph /\ k e. A ) -> B e. V )
rlimabs.2 
|- ( ph -> ( k e. A |-> B ) ~~>r C )
Assertion rlimmptrcl 
|- ( ( ph /\ k e. A ) -> B e. CC )

Proof

Step Hyp Ref Expression
1 rlimabs.1 
 |-  ( ( ph /\ k e. A ) -> B e. V )
2 rlimabs.2 
 |-  ( ph -> ( k e. A |-> B ) ~~>r C )
3 rlimf 
 |-  ( ( k e. A |-> B ) ~~>r C -> ( k e. A |-> B ) : dom ( k e. A |-> B ) --> CC )
4 2 3 syl 
 |-  ( ph -> ( k e. A |-> B ) : dom ( k e. A |-> B ) --> CC )
5 eqid 
 |-  ( k e. A |-> B ) = ( k e. A |-> B )
6 5 1 dmmptd 
 |-  ( ph -> dom ( k e. A |-> B ) = A )
7 6 feq2d 
 |-  ( ph -> ( ( k e. A |-> B ) : dom ( k e. A |-> B ) --> CC <-> ( k e. A |-> B ) : A --> CC ) )
8 4 7 mpbid 
 |-  ( ph -> ( k e. A |-> B ) : A --> CC )
9 8 fvmptelcdm 
 |-  ( ( ph /\ k e. A ) -> B e. CC )