Theorem fvtp3g

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	fvtp3g	⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝐶 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		tprot	⊢ { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } = { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ }
2	1	fveq1i	⊢ ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝐶 ) = ( { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ } ‘ 𝐶 )
3		necom	⊢ ( 𝐴 ≠ 𝐶 ↔ 𝐶 ≠ 𝐴 )
4		fvtp2g	⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) ∧ ( 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴 ) ) → ( { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ } ‘ 𝐶 ) = 𝐹 )
5	4	expcom	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐶 ≠ 𝐴 ) → ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) → ( { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ } ‘ 𝐶 ) = 𝐹 ) )
6	3 5	sylan2b	⊢ ( ( 𝐵 ≠ 𝐶 ∧ 𝐴 ≠ 𝐶 ) → ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) → ( { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ } ‘ 𝐶 ) = 𝐹 ) )
7	6	ancoms	⊢ ( ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) → ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) → ( { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ } ‘ 𝐶 ) = 𝐹 ) )
8	7	impcom	⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( { ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ , ⟨ 𝐴 , 𝐷 ⟩ } ‘ 𝐶 ) = 𝐹 )
9	2 8	syl5eq	⊢ ( ( ( 𝐶 ∈ 𝑉 ∧ 𝐹 ∈ 𝑊 ) ∧ ( 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( { ⟨ 𝐴 , 𝐷 ⟩ , ⟨ 𝐵 , 𝐸 ⟩ , ⟨ 𝐶 , 𝐹 ⟩ } ‘ 𝐶 ) = 𝐹 )