Metamath Proof Explorer

Theorem f13dfv

Description: A one-to-one function with a domain with at least three different elements in terms of function values. (Contributed by Alexander van der Vekens, 26-Jan-2018)

Ref Expression
Hypothesis f13dfv.a 
|- A = { X , Y , Z }
Assertion f13dfv 
|- ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( F : A -1-1-> B <-> ( F : A --> B /\ ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) ) )

Proof

Step Hyp Ref Expression
1 f13dfv.a 
 |-  A = { X , Y , Z }
2 dff14b 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) )
3 1 raleqi 
 |-  ( A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> A. x e. { X , Y , Z } A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) )
4 sneq 
 |-  ( x = X -> { x } = { X } )
5 4 difeq2d 
 |-  ( x = X -> ( A \ { x } ) = ( A \ { X } ) )
6 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
7 6 neeq1d 
 |-  ( x = X -> ( ( F ` x ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` y ) ) )
8 5 7 raleqbidv 
 |-  ( x = X -> ( A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) ) )
9 sneq 
 |-  ( x = Y -> { x } = { Y } )
10 9 difeq2d 
 |-  ( x = Y -> ( A \ { x } ) = ( A \ { Y } ) )
11 fveq2 
 |-  ( x = Y -> ( F ` x ) = ( F ` Y ) )
12 11 neeq1d 
 |-  ( x = Y -> ( ( F ` x ) =/= ( F ` y ) <-> ( F ` Y ) =/= ( F ` y ) ) )
13 10 12 raleqbidv 
 |-  ( x = Y -> ( A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) ) )
14 sneq 
 |-  ( x = Z -> { x } = { Z } )
15 14 difeq2d 
 |-  ( x = Z -> ( A \ { x } ) = ( A \ { Z } ) )
16 fveq2 
 |-  ( x = Z -> ( F ` x ) = ( F ` Z ) )
17 16 neeq1d 
 |-  ( x = Z -> ( ( F ` x ) =/= ( F ` y ) <-> ( F ` Z ) =/= ( F ` y ) ) )
18 15 17 raleqbidv 
 |-  ( x = Z -> ( A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> A. y e. ( A \ { Z } ) ( F ` Z ) =/= ( F ` y ) ) )
19 8 13 18 raltpg 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( A. x e. { X , Y , Z } A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) /\ A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) /\ A. y e. ( A \ { Z } ) ( F ` Z ) =/= ( F ` y ) ) ) )
20 19 adantr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. x e. { X , Y , Z } A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) /\ A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) /\ A. y e. ( A \ { Z } ) ( F ` Z ) =/= ( F ` y ) ) ) )
21 1 difeq1i 
 |-  ( A \ { X } ) = ( { X , Y , Z } \ { X } )
22 tprot 
 |-  { X , Y , Z } = { Y , Z , X }
23 22 difeq1i 
 |-  ( { X , Y , Z } \ { X } ) = ( { Y , Z , X } \ { X } )
24 necom 
 |-  ( X =/= Y <-> Y =/= X )
25 necom 
 |-  ( X =/= Z <-> Z =/= X )
26 24 25 anbi12i 
 |-  ( ( X =/= Y /\ X =/= Z ) <-> ( Y =/= X /\ Z =/= X ) )
27 26 biimpi 
 |-  ( ( X =/= Y /\ X =/= Z ) -> ( Y =/= X /\ Z =/= X ) )
28 27 3adant3 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( Y =/= X /\ Z =/= X ) )
29 diftpsn3 
 |-  ( ( Y =/= X /\ Z =/= X ) -> ( { Y , Z , X } \ { X } ) = { Y , Z } )
30 28 29 syl 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( { Y , Z , X } \ { X } ) = { Y , Z } )
31 23 30 eqtrid 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( { X , Y , Z } \ { X } ) = { Y , Z } )
32 21 31 eqtrid 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( A \ { X } ) = { Y , Z } )
33 32 adantl 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A \ { X } ) = { Y , Z } )
34 33 raleqdv 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) <-> A. y e. { Y , Z } ( F ` X ) =/= ( F ` y ) ) )
35 fveq2 
 |-  ( y = Y -> ( F ` y ) = ( F ` Y ) )
36 35 neeq2d 
 |-  ( y = Y -> ( ( F ` X ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` Y ) ) )
37 fveq2 
 |-  ( y = Z -> ( F ` y ) = ( F ` Z ) )
38 37 neeq2d 
 |-  ( y = Z -> ( ( F ` X ) =/= ( F ` y ) <-> ( F ` X ) =/= ( F ` Z ) ) )
39 36 38 ralprg 
 |-  ( ( Y e. V /\ Z e. W ) -> ( A. y e. { Y , Z } ( F ` X ) =/= ( F ` y ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) ) ) )
40 39 3adant1 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( A. y e. { Y , Z } ( F ` X ) =/= ( F ` y ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) ) ) )
41 40 adantr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. y e. { Y , Z } ( F ` X ) =/= ( F ` y ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) ) ) )
42 34 41 bitrd 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) ) ) )
43 1 difeq1i 
 |-  ( A \ { Y } ) = ( { X , Y , Z } \ { Y } )
44 tpcomb 
 |-  { X , Y , Z } = { X , Z , Y }
45 44 difeq1i 
 |-  ( { X , Y , Z } \ { Y } ) = ( { X , Z , Y } \ { Y } )
46 necom 
 |-  ( Y =/= Z <-> Z =/= Y )
47 46 biimpi 
 |-  ( Y =/= Z -> Z =/= Y )
48 47 anim2i 
 |-  ( ( X =/= Y /\ Y =/= Z ) -> ( X =/= Y /\ Z =/= Y ) )
49 48 3adant2 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( X =/= Y /\ Z =/= Y ) )
50 diftpsn3 
 |-  ( ( X =/= Y /\ Z =/= Y ) -> ( { X , Z , Y } \ { Y } ) = { X , Z } )
51 49 50 syl 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( { X , Z , Y } \ { Y } ) = { X , Z } )
52 45 51 eqtrid 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( { X , Y , Z } \ { Y } ) = { X , Z } )
53 43 52 eqtrid 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( A \ { Y } ) = { X , Z } )
54 53 adantl 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A \ { Y } ) = { X , Z } )
55 54 raleqdv 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) <-> A. y e. { X , Z } ( F ` Y ) =/= ( F ` y ) ) )
56 fveq2 
 |-  ( y = X -> ( F ` y ) = ( F ` X ) )
57 56 neeq2d 
 |-  ( y = X -> ( ( F ` Y ) =/= ( F ` y ) <-> ( F ` Y ) =/= ( F ` X ) ) )
58 37 neeq2d 
 |-  ( y = Z -> ( ( F ` Y ) =/= ( F ` y ) <-> ( F ` Y ) =/= ( F ` Z ) ) )
59 57 58 ralprg 
 |-  ( ( X e. U /\ Z e. W ) -> ( A. y e. { X , Z } ( F ` Y ) =/= ( F ` y ) <-> ( ( F ` Y ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) )
60 59 3adant2 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( A. y e. { X , Z } ( F ` Y ) =/= ( F ` y ) <-> ( ( F ` Y ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) )
61 60 adantr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. y e. { X , Z } ( F ` Y ) =/= ( F ` y ) <-> ( ( F ` Y ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) )
62 55 61 bitrd 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) <-> ( ( F ` Y ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) )
63 1 difeq1i 
 |-  ( A \ { Z } ) = ( { X , Y , Z } \ { Z } )
64 diftpsn3 
 |-  ( ( X =/= Z /\ Y =/= Z ) -> ( { X , Y , Z } \ { Z } ) = { X , Y } )
65 64 3adant1 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( { X , Y , Z } \ { Z } ) = { X , Y } )
66 63 65 eqtrid 
 |-  ( ( X =/= Y /\ X =/= Z /\ Y =/= Z ) -> ( A \ { Z } ) = { X , Y } )
67 66 adantl 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A \ { Z } ) = { X , Y } )
68 67 raleqdv 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. y e. ( A \ { Z } ) ( F ` Z ) =/= ( F ` y ) <-> A. y e. { X , Y } ( F ` Z ) =/= ( F ` y ) ) )
69 56 neeq2d 
 |-  ( y = X -> ( ( F ` Z ) =/= ( F ` y ) <-> ( F ` Z ) =/= ( F ` X ) ) )
70 35 neeq2d 
 |-  ( y = Y -> ( ( F ` Z ) =/= ( F ` y ) <-> ( F ` Z ) =/= ( F ` Y ) ) )
71 69 70 ralprg 
 |-  ( ( X e. U /\ Y e. V ) -> ( A. y e. { X , Y } ( F ` Z ) =/= ( F ` y ) <-> ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) )
72 71 3adant3 
 |-  ( ( X e. U /\ Y e. V /\ Z e. W ) -> ( A. y e. { X , Y } ( F ` Z ) =/= ( F ` y ) <-> ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) )
73 72 adantr 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. y e. { X , Y } ( F ` Z ) =/= ( F ` y ) <-> ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) )
74 68 73 bitrd 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. y e. ( A \ { Z } ) ( F ` Z ) =/= ( F ` y ) <-> ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) )
75 42 62 74 3anbi123d 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) /\ A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) /\ A. y e. ( A \ { Z } ) ( F ` Z ) =/= ( F ` y ) ) <-> ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) ) /\ ( ( F ` Y ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) /\ ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) ) )
76 ancom 
 |-  ( ( ( F ` Y ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) <-> ( ( F ` Y ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` X ) ) )
77 76 3anbi2i 
 |-  ( ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) ) /\ ( ( F ` Y ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) /\ ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) <-> ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) ) /\ ( ( F ` Y ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` X ) ) /\ ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) )
78 3an6 
 |-  ( ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) ) /\ ( ( F ` Y ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` X ) ) /\ ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) <-> ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) /\ ( F ` Z ) =/= ( F ` X ) ) /\ ( ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) )
79 3anrot 
 |-  ( ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) /\ ( F ` Z ) =/= ( F ` X ) ) )
80 79 bicomi 
 |-  ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) /\ ( F ` Z ) =/= ( F ` X ) ) <-> ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) )
81 necom 
 |-  ( ( F ` X ) =/= ( F ` Z ) <-> ( F ` Z ) =/= ( F ` X ) )
82 necom 
 |-  ( ( F ` Y ) =/= ( F ` X ) <-> ( F ` X ) =/= ( F ` Y ) )
83 necom 
 |-  ( ( F ` Z ) =/= ( F ` Y ) <-> ( F ` Y ) =/= ( F ` Z ) )
84 81 82 83 3anbi123i 
 |-  ( ( ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) <-> ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) )
85 80 84 anbi12i 
 |-  ( ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) /\ ( F ` Z ) =/= ( F ` X ) ) /\ ( ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) <-> ( ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) /\ ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) )
86 anidm 
 |-  ( ( ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) /\ ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) <-> ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) )
87 3ancoma 
 |-  ( ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` Z ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) )
88 necom 
 |-  ( ( F ` Z ) =/= ( F ` X ) <-> ( F ` X ) =/= ( F ` Z ) )
89 88 3anbi2i 
 |-  ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` Z ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) )
90 87 89 bitri 
 |-  ( ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) )
91 85 86 90 3bitri 
 |-  ( ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` Y ) =/= ( F ` Z ) /\ ( F ` Z ) =/= ( F ` X ) ) /\ ( ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) )
92 77 78 91 3bitri 
 |-  ( ( ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) ) /\ ( ( F ` Y ) =/= ( F ` X ) /\ ( F ` Y ) =/= ( F ` Z ) ) /\ ( ( F ` Z ) =/= ( F ` X ) /\ ( F ` Z ) =/= ( F ` Y ) ) ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) )
93 75 92 bitrdi 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( A. y e. ( A \ { X } ) ( F ` X ) =/= ( F ` y ) /\ A. y e. ( A \ { Y } ) ( F ` Y ) =/= ( F ` y ) /\ A. y e. ( A \ { Z } ) ( F ` Z ) =/= ( F ` y ) ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) )
94 20 93 bitrd 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. x e. { X , Y , Z } A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) )
95 3 94 bitrid 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) <-> ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) )
96 95 anbi2d 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( ( F : A --> B /\ A. x e. A A. y e. ( A \ { x } ) ( F ` x ) =/= ( F ` y ) ) <-> ( F : A --> B /\ ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) ) )
97 2 96 bitrid 
 |-  ( ( ( X e. U /\ Y e. V /\ Z e. W ) /\ ( X =/= Y /\ X =/= Z /\ Y =/= Z ) ) -> ( F : A -1-1-> B <-> ( F : A --> B /\ ( ( F ` X ) =/= ( F ` Y ) /\ ( F ` X ) =/= ( F ` Z ) /\ ( F ` Y ) =/= ( F ` Z ) ) ) ) )