Theorem rlimmptrcl

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

	Ref	Expression
Hypotheses	rlimabs.1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	rlimabs.2	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
Assertion	rlimmptrcl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		rlimabs.1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		rlimabs.2	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
3		rlimf	⊢ ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℂ )
4	2 3	syl	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℂ )
5		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
6	5 1	dmmptd	⊢ ( 𝜑 → dom ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
7	6	feq2d	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℂ ↔ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ) )
8	4 7	mpbid	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
9	8	fvmptelrn	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )