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 ⊢ Ⅎ 𝑥 𝜑
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 𝐹 = ∅ ↔ 𝐴 = ∅ ) )