Theorem fvtp0

Description: The undefined value of a function with a domain of three elements. (Contributed by AV, 18-Aug-2026)

	Ref	Expression
Hypotheses	fvtp0.d	$$⊢D\in \mathrm{V}$$
	fvtp0.e	$$⊢E\in \mathrm{V}$$
	fvtp0.f	$$⊢F\in \mathrm{V}$$
	fvtp0.x	$$⊢X\in \mathrm{V}$$
Assertion	fvtp0	$$⊢\left(X\ne A\wedge X\ne B\wedge X\ne C\right)\to \left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\left(X\right)=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		fvtp0.d	$$⊢D\in \mathrm{V}$$
2		fvtp0.e	$$⊢E\in \mathrm{V}$$
3		fvtp0.f	$$⊢F\in \mathrm{V}$$
4		fvtp0.x	$$⊢X\in \mathrm{V}$$
5		df-ne	$$⊢X\ne A\leftrightarrow \neg X=A$$
6		df-ne	$$⊢X\ne B\leftrightarrow \neg X=B$$
7		df-ne	$$⊢X\ne C\leftrightarrow \neg X=C$$
8	5 6 7	3anbi123i	$$⊢\left(X\ne A\wedge X\ne B\wedge X\ne C\right)\leftrightarrow \left(\neg X=A\wedge \neg X=B\wedge \neg X=C\right)$$
9		3ioran	$$⊢\neg \left(X=A\vee X=B\vee X=C\right)\leftrightarrow \left(\neg X=A\wedge \neg X=B\wedge \neg X=C\right)$$
10	4	eltp	$$⊢X\in \left\{A,B,C\right\}\leftrightarrow \left(X=A\vee X=B\vee X=C\right)$$
11	9 10	xchnxbir	$$⊢\neg X\in \left\{A,B,C\right\}\leftrightarrow \left(\neg X=A\wedge \neg X=B\wedge \neg X=C\right)$$
12	8 11	sylbb2	$$⊢\left(X\ne A\wedge X\ne B\wedge X\ne C\right)\to \neg X\in \left\{A,B,C\right\}$$
13	1 2 3	dmtpop	$$⊢\mathrm{dom}\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}=\left\{A,B,C\right\}$$
14	13	eleq2i	$$⊢X\in \mathrm{dom}\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\leftrightarrow X\in \left\{A,B,C\right\}$$
15	12 14	sylnibr	$$⊢\left(X\ne A\wedge X\ne B\wedge X\ne C\right)\to \neg X\in \mathrm{dom}\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}$$
16		ndmfv	$$⊢\neg X\in \mathrm{dom}\left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\to \left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\left(X\right)=\varnothing$$
17	15 16	syl	$$⊢\left(X\ne A\wedge X\ne B\wedge X\ne C\right)\to \left\{⟨A,D⟩,⟨B,E⟩,⟨C,F⟩\right\}\left(X\right)=\varnothing$$