Theorem fvtp3

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

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

Proof

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