Theorem fvtp1g

Description: The value of a function with a domain of (at most) three elements. (Contributed by Alexander van der Vekens, 4-Dec-2017)

	Ref	Expression
Assertion	fvtp1g	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝐴 ) = 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		df-tp	⊢ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } = ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } )
2	1	fveq1i	⊢ ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝐴 ) = ( ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) ‘ 𝐴 )
3		necom	⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴 )
4		fvunsn	⊢ ( 𝐶 ≠ 𝐴 → ( ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ‘ 𝐴 ) )
5	3 4	sylbi	⊢ ( 𝐴 ≠ 𝐶 → ( ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ‘ 𝐴 ) )
6	5	ad2antll	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ) → ( ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) ‘ 𝐴 ) = ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ‘ 𝐴 ) )
7		fvpr1g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐷 )
8	7	3expa	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ 𝐴 ≠ 𝐵 ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐷 )
9	8	adantrr	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ‘ 𝐴 ) = 𝐷 )
10	6 9	eqtrd	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ) → ( ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ } ∪ { ⟨ 𝐶 , 𝐹 ⟩ } ) ‘ 𝐴 ) = 𝐷 )
11	2 10	syl5eq	⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ) ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝐴 ) = 𝐷 )