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	⊢ 𝐷 ∈ V
	fvtp0.e	⊢ 𝐸 ∈ V
	fvtp0.f	⊢ 𝐹 ∈ V
	fvtp0.x	⊢ 𝑋 ∈ V
Assertion	fvtp0	⊢ ( ( 𝑋 ≠ 𝐴 ∧ 𝑋 ≠ 𝐵 ∧ 𝑋 ≠ 𝐶 ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝑋 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		fvtp0.d	⊢ 𝐷 ∈ V
2		fvtp0.e	⊢ 𝐸 ∈ V
3		fvtp0.f	⊢ 𝐹 ∈ V
4		fvtp0.x	⊢ 𝑋 ∈ V
5		df-ne	⊢ ( 𝑋 ≠ 𝐴 ↔ ¬ 𝑋 = 𝐴 )
6		df-ne	⊢ ( 𝑋 ≠ 𝐵 ↔ ¬ 𝑋 = 𝐵 )
7		df-ne	⊢ ( 𝑋 ≠ 𝐶 ↔ ¬ 𝑋 = 𝐶 )
8	5 6 7	3anbi123i	⊢ ( ( 𝑋 ≠ 𝐴 ∧ 𝑋 ≠ 𝐵 ∧ 𝑋 ≠ 𝐶 ) ↔ ( ¬ 𝑋 = 𝐴 ∧ ¬ 𝑋 = 𝐵 ∧ ¬ 𝑋 = 𝐶 ) )
9		3ioran	⊢ ( ¬ ( 𝑋 = 𝐴 ∨ 𝑋 = 𝐵 ∨ 𝑋 = 𝐶 ) ↔ ( ¬ 𝑋 = 𝐴 ∧ ¬ 𝑋 = 𝐵 ∧ ¬ 𝑋 = 𝐶 ) )
10	4	eltp	⊢ ( 𝑋 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( 𝑋 = 𝐴 ∨ 𝑋 = 𝐵 ∨ 𝑋 = 𝐶 ) )
11	9 10	xchnxbir	⊢ ( ¬ 𝑋 ∈ { 𝐴 , 𝐵 , 𝐶 } ↔ ( ¬ 𝑋 = 𝐴 ∧ ¬ 𝑋 = 𝐵 ∧ ¬ 𝑋 = 𝐶 ) )
12	8 11	sylbb2	⊢ ( ( 𝑋 ≠ 𝐴 ∧ 𝑋 ≠ 𝐵 ∧ 𝑋 ≠ 𝐶 ) → ¬ 𝑋 ∈ { 𝐴 , 𝐵 , 𝐶 } )
13	1 2 3	dmtpop	⊢ dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } = { 𝐴 , 𝐵 , 𝐶 }
14	13	eleq2i	⊢ ( 𝑋 ∈ dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ↔ 𝑋 ∈ { 𝐴 , 𝐵 , 𝐶 } )
15	12 14	sylnibr	⊢ ( ( 𝑋 ≠ 𝐴 ∧ 𝑋 ≠ 𝐵 ∧ 𝑋 ≠ 𝐶 ) → ¬ 𝑋 ∈ dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } )
16		ndmfv	⊢ ( ¬ 𝑋 ∈ dom { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝑋 ) = ∅ )
17	15 16	syl	⊢ ( ( 𝑋 ≠ 𝐴 ∧ 𝑋 ≠ 𝐵 ∧ 𝑋 ≠ 𝐶 ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝑋 ) = ∅ )