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	$$⊢F=\left(x\in A⟼B\right)$$
	limcmptdm.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
	limcmptdm.c	$$⊢\phi \to C\in \left(F{lim}_{ℂ}D\right)$$
Assertion	limcmptdm	$$⊢\phi \to A\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		limcmptdm.f	$$⊢F=\left(x\in A⟼B\right)$$
2		limcmptdm.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
3		limcmptdm.c	$$⊢\phi \to C\in \left(F{lim}_{ℂ}D\right)$$
4	1 2	dmmptd	$$⊢\phi \to \mathrm{dom}F=A$$
5		limcrcl	$$⊢C\in \left(F{lim}_{ℂ}D\right)\to \left(F:\mathrm{dom}F⟶ℂ\wedge \mathrm{dom}F\subseteq ℂ\wedge D\in ℂ\right)$$
6	3 5	syl	$$⊢\phi \to \left(F:\mathrm{dom}F⟶ℂ\wedge \mathrm{dom}F\subseteq ℂ\wedge D\in ℂ\right)$$
7	6	simp2d	$$⊢\phi \to \mathrm{dom}F\subseteq ℂ$$
8	4 7	eqsstrrd	$$⊢\phi \to A\subseteq ℂ$$