Theorem nelrnmpt

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

	Ref	Expression
Hypotheses	nelrnmpt.x	⊢ Ⅎ 𝑥 𝜑
	nelrnmpt.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	nelrnmpt.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	nelrnmpt.n	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 𝐵 )
Assertion	nelrnmpt	⊢ ( 𝜑 → ¬ 𝐶 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		nelrnmpt.x	⊢ Ⅎ 𝑥 𝜑
2		nelrnmpt.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3		nelrnmpt.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
4		nelrnmpt.n	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ≠ 𝐵 )
5	4	neneqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ¬ 𝐶 = 𝐵 )
6	5	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → ¬ 𝐶 = 𝐵 ) )
7	1 6	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ¬ 𝐶 = 𝐵 )
8		ralnex	⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝐶 = 𝐵 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )
9	7 8	sylib	⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )
10	2	elrnmpt	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
11	3 10	syl	⊢ ( 𝜑 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
12	9 11	mtbird	⊢ ( 𝜑 → ¬ 𝐶 ∈ ran 𝐹 )