Metamath Proof Explorer

Theorem f13idfv

Description: A one-to-one function with the domain { 0, 1 ,2 } in terms of function values. (Contributed by Alexander van der Vekens, 26-Jan-2018)

Ref Expression
Hypothesis f13idfv.a 
|- A = ( 0 ... 2 )
Assertion f13idfv 
|- ( F : A -1-1-> B <-> ( F : A --> B /\ ( ( F ` 0 ) =/= ( F ` 1 ) /\ ( F ` 0 ) =/= ( F ` 2 ) /\ ( F ` 1 ) =/= ( F ` 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 f13idfv.a 
 |-  A = ( 0 ... 2 )
2 0z 
 |-  0 e. ZZ
3 1z 
 |-  1 e. ZZ
4 2z 
 |-  2 e. ZZ
5 2 3 4 3pm3.2i 
 |-  ( 0 e. ZZ /\ 1 e. ZZ /\ 2 e. ZZ )
6 0ne1 
 |-  0 =/= 1
7 0ne2 
 |-  0 =/= 2
8 1ne2 
 |-  1 =/= 2
9 6 7 8 3pm3.2i 
 |-  ( 0 =/= 1 /\ 0 =/= 2 /\ 1 =/= 2 )
10 fz0tp 
 |-  ( 0 ... 2 ) = { 0 , 1 , 2 }
11 1 10 eqtri 
 |-  A = { 0 , 1 , 2 }
12 11 f13dfv 
 |-  ( ( ( 0 e. ZZ /\ 1 e. ZZ /\ 2 e. ZZ ) /\ ( 0 =/= 1 /\ 0 =/= 2 /\ 1 =/= 2 ) ) -> ( F : A -1-1-> B <-> ( F : A --> B /\ ( ( F ` 0 ) =/= ( F ` 1 ) /\ ( F ` 0 ) =/= ( F ` 2 ) /\ ( F ` 1 ) =/= ( F ` 2 ) ) ) ) )
13 5 9 12 mp2an 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ ( ( F ` 0 ) =/= ( F ` 1 ) /\ ( F ` 0 ) =/= ( F ` 2 ) /\ ( F ` 1 ) =/= ( F ` 2 ) ) ) )