Theorem rlimmptrcl

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

	Ref	Expression
Hypotheses	rlimabs.1	$$⊢\left(\phi \wedge k\in A\right)\to B\in V$$
	rlimabs.2	$$⊢\phi \to \left(k\in A⟼B\right)\underset{ℝ}{⇝}C$$
Assertion	rlimmptrcl	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		rlimabs.1	$$⊢\left(\phi \wedge k\in A\right)\to B\in V$$
2		rlimabs.2	$$⊢\phi \to \left(k\in A⟼B\right)\underset{ℝ}{⇝}C$$
3		rlimf	$$⊢\left(k\in A⟼B\right)\underset{ℝ}{⇝}C\to \left(k\in A⟼B\right):\mathrm{dom}\left(k\in A⟼B\right)⟶ℂ$$
4	2 3	syl	$$⊢\phi \to \left(k\in A⟼B\right):\mathrm{dom}\left(k\in A⟼B\right)⟶ℂ$$
5		eqid	$$⊢\left(k\in A⟼B\right)=\left(k\in A⟼B\right)$$
6	5 1	dmmptd	$$⊢\phi \to \mathrm{dom}\left(k\in A⟼B\right)=A$$
7	6	feq2d	$$⊢\phi \to \left(\left(k\in A⟼B\right):\mathrm{dom}\left(k\in A⟼B\right)⟶ℂ\leftrightarrow \left(k\in A⟼B\right):A⟶ℂ\right)$$
8	4 7	mpbid	$$⊢\phi \to \left(k\in A⟼B\right):A⟶ℂ$$
9	8	fvmptelrn	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$