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 e. _V
	fvtp0.e	|- E e. _V
	fvtp0.f	|- F e. _V
	fvtp0.x	|- X e. _V
Assertion	fvtp0	|- ( ( X =/= A /\ X =/= B /\ X =/= C ) -> ( { <. A , D >. , <. B , E >. , <. C , F >. } ` X ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		fvtp0.d	|- D e. _V
2		fvtp0.e	|- E e. _V
3		fvtp0.f	|- F e. _V
4		fvtp0.x	|- X e. _V
5		df-ne	|- ( X =/= A <-> -. X = A )
6		df-ne	|- ( X =/= B <-> -. X = B )
7		df-ne	|- ( X =/= C <-> -. X = C )
8	5 6 7	3anbi123i	|- ( ( X =/= A /\ X =/= B /\ X =/= C ) <-> ( -. X = A /\ -. X = B /\ -. X = C ) )
9		3ioran	|- ( -. ( X = A \/ X = B \/ X = C ) <-> ( -. X = A /\ -. X = B /\ -. X = C ) )
10	4	eltp	|- ( X e. { A , B , C } <-> ( X = A \/ X = B \/ X = C ) )
11	9 10	xchnxbir	|- ( -. X e. { A , B , C } <-> ( -. X = A /\ -. X = B /\ -. X = C ) )
12	8 11	sylbb2	|- ( ( X =/= A /\ X =/= B /\ X =/= C ) -> -. X e. { A , B , C } )
13	1 2 3	dmtpop	|- dom { <. A , D >. , <. B , E >. , <. C , F >. } = { A , B , C }
14	13	eleq2i	|- ( X e. dom { <. A , D >. , <. B , E >. , <. C , F >. } <-> X e. { A , B , C } )
15	12 14	sylnibr	|- ( ( X =/= A /\ X =/= B /\ X =/= C ) -> -. X e. dom { <. A , D >. , <. B , E >. , <. C , F >. } )
16		ndmfv	|- ( -. X e. dom { <. A , D >. , <. B , E >. , <. C , F >. } -> ( { <. A , D >. , <. B , E >. , <. C , F >. } ` X ) = (/) )
17	15 16	syl	|- ( ( X =/= A /\ X =/= B /\ X =/= C ) -> ( { <. A , D >. , <. B , E >. , <. C , F >. } ` X ) = (/) )