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

Metamath Proof Explorer

Theorem rnmptn0

Description: The range of a function in maps-to notation is nonempty if the domain is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses rnmpt0f.1 ⊢ Ⅎ 𝑥 𝜑
rnmpt0f.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
rnmpt0f.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
rnmptn0.a ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
Assertion rnmptn0 ( 𝜑 → ran 𝐹 ≠ ∅ )

Proof

Step Hyp Ref Expression
1 rnmpt0f.1 ⊢ Ⅎ 𝑥 𝜑
2 rnmpt0f.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 rnmpt0f.3 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
4 rnmptn0.a ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
5 4 neneqd ⊢ ( 𝜑 → ¬ 𝐴 = ∅ )
6 1 2 3 rnmpt0f ⊢ ( 𝜑 → ( ran 𝐹 = ∅ ↔ 𝐴 = ∅ ) )
7 5 6 mtbird ⊢ ( 𝜑 → ¬ ran 𝐹 = ∅ )
8 7 neqned ⊢ ( 𝜑 → ran 𝐹 ≠ ∅ )