This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = (/) ) )