Theorem rnmpt0f

Description: The range of a function in maps-to notation is empty if and only if its domain is empty. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	rnmpt0f.1	|- F/ x ph
	rnmpt0f.2	|- ( ( ph /\ x e. A ) -> B e. V )
	rnmpt0f.3	|- F = ( x e. A |-> B )
Assertion	rnmpt0f	|- ( ph -> ( ran F = (/) <-> A = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		rnmpt0f.1	|- F/ x ph
2		rnmpt0f.2	|- ( ( ph /\ x e. A ) -> B e. V )
3		rnmpt0f.3	|- F = ( x e. A |-> B )
4	2	ex	|- ( ph -> ( x e. A -> B e. V ) )
5	1 4	ralrimi	|- ( ph -> A. x e. A B e. V )
6		dmmptg	|- ( A. x e. A B e. V -> dom ( x e. A |-> B ) = A )
7	5 6	syl	|- ( ph -> dom ( x e. A |-> B ) = A )
8	7	eqcomd	|- ( ph -> A = dom ( x e. A |-> B ) )
9	8	eqeq1d	|- ( ph -> ( A = (/) <-> dom ( x e. A |-> B ) = (/) ) )
10		dm0rn0	|- ( dom ( x e. A |-> B ) = (/) <-> ran ( x e. A |-> B ) = (/) )
11	10	a1i	|- ( ph -> ( dom ( x e. A |-> B ) = (/) <-> ran ( x e. A |-> B ) = (/) ) )
12	3	rneqi	|- ran F = ran ( x e. A |-> B )
13	12	a1i	|- ( ph -> ran F = ran ( x e. A |-> B ) )
14	13	eqcomd	|- ( ph -> ran ( x e. A |-> B ) = ran F )
15	14	eqeq1d	|- ( ph -> ( ran ( x e. A |-> B ) = (/) <-> ran F = (/) ) )
16	9 11 15	3bitrrd	|- ( ph -> ( ran F = (/) <-> A = (/) ) )