Theorem fvtp1

Description: The first value of a function with a domain of three elements. (Contributed by NM, 14-Sep-2011)

	Ref	Expression
Hypotheses	fvtp1.1	⊢ 𝐴 ∈ V
	fvtp1.4	⊢ 𝐷 ∈ V
Assertion	fvtp1	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝐴 ) = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		fvtp1.1	⊢ 𝐴 ∈ V
2		fvtp1.4	⊢ 𝐷 ∈ V
3		df-tp	⊢ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } = ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } )
4	3	fveq1i	⊢ ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝐴 ) = ( ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) ‘ 𝐴 )
5		necom	⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴 )
6		fvunsn	⊢ ( 𝐶 ≠ 𝐴 → ( ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ‘ 𝐴 ) )
7	5 6	sylbi	⊢ ( 𝐴 ≠ 𝐶 → ( ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ‘ 𝐴 ) )
8	1 2	fvpr1	⊢ ( 𝐴 ≠ 𝐵 → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐷 )
9	7 8	sylan9eqr	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) ‘ 𝐴 ) = 𝐷 )
10	4 9	syl5eq	⊢ ( ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝐴 ) = 𝐷 )