Metamath Proof Explorer

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 
|- C e. _V
fvtp3.4 
|- F e. _V
Assertion fvtp3 
|- ( ( A =/= C /\ B =/= C ) -> ( { <. A , D >. , <. B , E >. , <. C , F >. } ` C ) = F )

Proof

Step Hyp Ref Expression
1 fvtp3.1 
 |-  C e. _V
2 fvtp3.4 
 |-  F e. _V
3 tprot 
 |-  { <. A , D >. , <. B , E >. , <. C , F >. } = { <. B , E >. , <. C , F >. , <. A , D >. }
4 3 fveq1i 
 |-  ( { <. A , D >. , <. B , E >. , <. C , F >. } ` C ) = ( { <. B , E >. , <. C , F >. , <. A , D >. } ` C )
5 necom 
 |-  ( A =/= C <-> C =/= A )
6 1 2 fvtp2 
 |-  ( ( B =/= C /\ C =/= A ) -> ( { <. B , E >. , <. C , F >. , <. A , D >. } ` C ) = F )
7 5 6 sylan2b 
 |-  ( ( B =/= C /\ A =/= C ) -> ( { <. B , E >. , <. C , F >. , <. A , D >. } ` C ) = F )
8 7 ancoms 
 |-  ( ( A =/= C /\ B =/= C ) -> ( { <. B , E >. , <. C , F >. , <. A , D >. } ` C ) = F )
9 4 8 syl5eq 
 |-  ( ( A =/= C /\ B =/= C ) -> ( { <. A , D >. , <. B , E >. , <. C , F >. } ` C ) = F )