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 𝑥 𝜑
rnmpt0f.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
rnmpt0f.3 𝐹 = ( 𝑥𝐴𝐵 )
Assertion rnmpt0f ( 𝜑 → ( ran 𝐹 = ∅ ↔ 𝐴 = ∅ ) )

Proof

Step Hyp Ref Expression
1 rnmpt0f.1 𝑥 𝜑
2 rnmpt0f.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
3 rnmpt0f.3 𝐹 = ( 𝑥𝐴𝐵 )
4 2 ex ( 𝜑 → ( 𝑥𝐴𝐵𝑉 ) )
5 1 4 ralrimi ( 𝜑 → ∀ 𝑥𝐴 𝐵𝑉 )
6 dmmptg ( ∀ 𝑥𝐴 𝐵𝑉 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
7 5 6 syl ( 𝜑 → dom ( 𝑥𝐴𝐵 ) = 𝐴 )
8 7 eqcomd ( 𝜑𝐴 = dom ( 𝑥𝐴𝐵 ) )
9 8 eqeq1d ( 𝜑 → ( 𝐴 = ∅ ↔ dom ( 𝑥𝐴𝐵 ) = ∅ ) )
10 dm0rn0 ( dom ( 𝑥𝐴𝐵 ) = ∅ ↔ ran ( 𝑥𝐴𝐵 ) = ∅ )
11 10 a1i ( 𝜑 → ( dom ( 𝑥𝐴𝐵 ) = ∅ ↔ ran ( 𝑥𝐴𝐵 ) = ∅ ) )
12 3 rneqi ran 𝐹 = ran ( 𝑥𝐴𝐵 )
13 12 a1i ( 𝜑 → ran 𝐹 = ran ( 𝑥𝐴𝐵 ) )
14 13 eqcomd ( 𝜑 → ran ( 𝑥𝐴𝐵 ) = ran 𝐹 )
15 14 eqeq1d ( 𝜑 → ( ran ( 𝑥𝐴𝐵 ) = ∅ ↔ ran 𝐹 = ∅ ) )
16 9 11 15 3bitrrd ( 𝜑 → ( ran 𝐹 = ∅ ↔ 𝐴 = ∅ ) )