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 𝐹 = ∅ ↔ 𝐴 = ∅ ) )