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 )