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 = ( x e. A |-> B )
	limcmptdm.b	|- ( ( ph /\ x e. A ) -> B e. CC )
	limcmptdm.c	|- ( ph -> C e. ( F limCC D ) )
Assertion	limcmptdm	|- ( ph -> A C_ CC )

Proof

Step	Hyp	Ref	Expression
1		limcmptdm.f	|- F = ( x e. A |-> B )
2		limcmptdm.b	|- ( ( ph /\ x e. A ) -> B e. CC )
3		limcmptdm.c	|- ( ph -> C e. ( F limCC D ) )
4	1 2	dmmptd	|- ( ph -> dom F = A )
5		limcrcl	|- ( C e. ( F limCC D ) -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
6	3 5	syl	|- ( ph -> ( F : dom F --> CC /\ dom F C_ CC /\ D e. CC ) )
7	6	simp2d	|- ( ph -> dom F C_ CC )
8	4 7	eqsstrrd	|- ( ph -> A C_ CC )