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	$$⊢Ⅎx\phi$$
	nelrnmpt.f	$$⊢F=\left(x\in A⟼B\right)$$
	nelrnmpt.c	$$⊢\phi \to C\in V$$
	nelrnmpt.n	$$⊢\left(\phi \wedge x\in A\right)\to C\ne B$$
Assertion	nelrnmpt	$$⊢\phi \to \neg C\in \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		nelrnmpt.x	$$⊢Ⅎx\phi$$
2		nelrnmpt.f	$$⊢F=\left(x\in A⟼B\right)$$
3		nelrnmpt.c	$$⊢\phi \to C\in V$$
4		nelrnmpt.n	$$⊢\left(\phi \wedge x\in A\right)\to C\ne B$$
5	4	neneqd	$$⊢\left(\phi \wedge x\in A\right)\to \neg C=B$$
6	5	ex	$$⊢\phi \to \left(x\in A\to \neg C=B\right)$$
7	1 6	ralrimi	$$⊢\phi \to \forall x\in A\neg C=B$$
8		ralnex	$$⊢\forall x\in A\neg C=B\leftrightarrow \neg \exists x\in AC=B$$
9	7 8	sylib	$$⊢\phi \to \neg \exists x\in AC=B$$
10	2	elrnmpt	$$⊢C\in V\to \left(C\in \mathrm{ran}F\leftrightarrow \exists x\in AC=B\right)$$
11	3 10	syl	$$⊢\phi \to \left(C\in \mathrm{ran}F\leftrightarrow \exists x\in AC=B\right)$$
12	9 11	mtbird	$$⊢\phi \to \neg C\in \mathrm{ran}F$$