Metamath Proof Explorer

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

Proof

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