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

Metamath Proof Explorer

Theorem nelrnmpt

Description: Non-membership in the range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses nelrnmpt.x ⊢ Ⅎ x φ
nelrnmpt.f ⊢ F = x ∈ A ⟼ B
nelrnmpt.c ⊢ φ → C ∈ V
nelrnmpt.n ⊢ φ ∧ x ∈ A → C ≠ B
Assertion nelrnmpt ⊢ φ → ¬ C ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 nelrnmpt.x ⊢ Ⅎ x φ
2 nelrnmpt.f ⊢ F = x ∈ A ⟼ B
3 nelrnmpt.c ⊢ φ → C ∈ V
4 nelrnmpt.n ⊢ φ ∧ x ∈ A → C ≠ B
5 4 neneqd ⊢ φ ∧ x ∈ A → ¬ C = B
6 5 ex ⊢ φ → x ∈ A → ¬ C = B
7 1 6 ralrimi ⊢ φ → ∀ x ∈ A ¬ C = B
8 ralnex ⊢ ∀ x ∈ A ¬ C = B ↔ ¬ ∃ x ∈ A C = B
9 7 8 sylib ⊢ φ → ¬ ∃ x ∈ A C = B
10 2 elrnmpt ⊢ C ∈ V → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B
11 3 10 syl ⊢ φ → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B
12 9 11 mtbird ⊢ φ → ¬ C ∈ ran ⁡ F