Theorem limcmptdm

Description: The domain of a maps-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	limcmptdm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	limcmptdm.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
	limcmptdm.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) )
Assertion	limcmptdm	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )

Proof

Step	Hyp	Ref	Expression
1		limcmptdm.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		limcmptdm.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
3		limcmptdm.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) )
4	1 2	dmmptd	⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
5		limcrcl	⊢ ( 𝐶 ∈ ( 𝐹 limℂ 𝐷 ) → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
6	3 5	syl	⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐷 ∈ ℂ ) )
7	6	simp2d	⊢ ( 𝜑 → dom 𝐹 ⊆ ℂ )
8	4 7	eqsstrrd	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )