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 ⊢ Ⅎ x φ
rnmpt0f.2 ⊢ φ ∧ x ∈ A → B ∈ V
rnmpt0f.3 ⊢ F = x ∈ A ⟼ B
Assertion rnmpt0f ⊢ φ → ran ⁡ F = ∅ ↔ A = ∅

Proof

Step Hyp Ref Expression
1 rnmpt0f.1 ⊢ Ⅎ x φ
2 rnmpt0f.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 rnmpt0f.3 ⊢ F = x ∈ A ⟼ B
4 2 ex ⊢ φ → x ∈ A → B ∈ V
5 1 4 ralrimi ⊢ φ → ∀ x ∈ A B ∈ V
6 dmmptg ⊢ ∀ x ∈ A B ∈ V → dom ⁡ x ∈ A ⟼ B = A
7 5 6 syl ⊢ φ → dom ⁡ x ∈ A ⟼ B = A
8 7 eqcomd ⊢ φ → A = dom ⁡ x ∈ A ⟼ B
9 8 eqeq1d ⊢ φ → A = ∅ ↔ dom ⁡ x ∈ A ⟼ B = ∅
10 dm0rn0 ⊢ dom ⁡ x ∈ A ⟼ B = ∅ ↔ ran ⁡ x ∈ A ⟼ B = ∅
11 10 a1i ⊢ φ → dom ⁡ x ∈ A ⟼ B = ∅ ↔ ran ⁡ x ∈ A ⟼ B = ∅
12 3 rneqi ⊢ ran ⁡ F = ran ⁡ x ∈ A ⟼ B
13 12 a1i ⊢ φ → ran ⁡ F = ran ⁡ x ∈ A ⟼ B
14 13 eqcomd ⊢ φ → ran ⁡ x ∈ A ⟼ B = ran ⁡ F
15 14 eqeq1d ⊢ φ → ran ⁡ x ∈ A ⟼ B = ∅ ↔ ran ⁡ F = ∅
16 9 11 15 3bitrrd ⊢ φ → ran ⁡ F = ∅ ↔ A = ∅