Metamath Proof Explorer

Theorem dff13

Description: A one-to-one function in terms of function values. Compare Theorem 4.8(iv) of Monk1 p. 43. (Contributed by NM, 29-Oct-1996)

Ref Expression
Assertion dff13 
|- ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )

Proof

Step Hyp Ref Expression
1 dff12 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. z E* x x F z ) )
2 ffn 
 |-  ( F : A --> B -> F Fn A )
3 vex 
 |-  x e. _V
4 vex 
 |-  z e. _V
5 3 4 breldm 
 |-  ( x F z -> x e. dom F )
6 fndm 
 |-  ( F Fn A -> dom F = A )
7 6 eleq2d 
 |-  ( F Fn A -> ( x e. dom F <-> x e. A ) )
8 5 7 imbitrid 
 |-  ( F Fn A -> ( x F z -> x e. A ) )
9 vex 
 |-  y e. _V
10 9 4 breldm 
 |-  ( y F z -> y e. dom F )
11 6 eleq2d 
 |-  ( F Fn A -> ( y e. dom F <-> y e. A ) )
12 10 11 imbitrid 
 |-  ( F Fn A -> ( y F z -> y e. A ) )
13 8 12 anim12d 
 |-  ( F Fn A -> ( ( x F z /\ y F z ) -> ( x e. A /\ y e. A ) ) )
14 13 pm4.71rd 
 |-  ( F Fn A -> ( ( x F z /\ y F z ) <-> ( ( x e. A /\ y e. A ) /\ ( x F z /\ y F z ) ) ) )
15 eqcom 
 |-  ( z = ( F ` x ) <-> ( F ` x ) = z )
16 fnbrfvb 
 |-  ( ( F Fn A /\ x e. A ) -> ( ( F ` x ) = z <-> x F z ) )
17 15 16 bitrid 
 |-  ( ( F Fn A /\ x e. A ) -> ( z = ( F ` x ) <-> x F z ) )
18 eqcom 
 |-  ( z = ( F ` y ) <-> ( F ` y ) = z )
19 fnbrfvb 
 |-  ( ( F Fn A /\ y e. A ) -> ( ( F ` y ) = z <-> y F z ) )
20 18 19 bitrid 
 |-  ( ( F Fn A /\ y e. A ) -> ( z = ( F ` y ) <-> y F z ) )
21 17 20 bi2anan9 
 |-  ( ( ( F Fn A /\ x e. A ) /\ ( F Fn A /\ y e. A ) ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) <-> ( x F z /\ y F z ) ) )
22 21 anandis 
 |-  ( ( F Fn A /\ ( x e. A /\ y e. A ) ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) <-> ( x F z /\ y F z ) ) )
23 22 pm5.32da 
 |-  ( F Fn A -> ( ( ( x e. A /\ y e. A ) /\ ( z = ( F ` x ) /\ z = ( F ` y ) ) ) <-> ( ( x e. A /\ y e. A ) /\ ( x F z /\ y F z ) ) ) )
24 14 23 bitr4d 
 |-  ( F Fn A -> ( ( x F z /\ y F z ) <-> ( ( x e. A /\ y e. A ) /\ ( z = ( F ` x ) /\ z = ( F ` y ) ) ) ) )
25 24 imbi1d 
 |-  ( F Fn A -> ( ( ( x F z /\ y F z ) -> x = y ) <-> ( ( ( x e. A /\ y e. A ) /\ ( z = ( F ` x ) /\ z = ( F ` y ) ) ) -> x = y ) ) )
26 impexp 
 |-  ( ( ( ( x e. A /\ y e. A ) /\ ( z = ( F ` x ) /\ z = ( F ` y ) ) ) -> x = y ) <-> ( ( x e. A /\ y e. A ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) )
27 25 26 bitrdi 
 |-  ( F Fn A -> ( ( ( x F z /\ y F z ) -> x = y ) <-> ( ( x e. A /\ y e. A ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) ) )
28 27 albidv 
 |-  ( F Fn A -> ( A. z ( ( x F z /\ y F z ) -> x = y ) <-> A. z ( ( x e. A /\ y e. A ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) ) )
29 19.21v 
 |-  ( A. z ( ( x e. A /\ y e. A ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) <-> ( ( x e. A /\ y e. A ) -> A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) )
30 19.23v 
 |-  ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
31 fvex 
 |-  ( F ` x ) e. _V
32 31 eqvinc 
 |-  ( ( F ` x ) = ( F ` y ) <-> E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) )
33 32 imbi1i 
 |-  ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> ( E. z ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) )
34 30 33 bitr4i 
 |-  ( A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) <-> ( ( F ` x ) = ( F ` y ) -> x = y ) )
35 34 imbi2i 
 |-  ( ( ( x e. A /\ y e. A ) -> A. z ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) <-> ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
36 29 35 bitri 
 |-  ( A. z ( ( x e. A /\ y e. A ) -> ( ( z = ( F ` x ) /\ z = ( F ` y ) ) -> x = y ) ) <-> ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
37 28 36 bitrdi 
 |-  ( F Fn A -> ( A. z ( ( x F z /\ y F z ) -> x = y ) <-> ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) )
38 37 2albidv 
 |-  ( F Fn A -> ( A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) ) )
39 breq1 
 |-  ( x = y -> ( x F z <-> y F z ) )
40 39 mo4 
 |-  ( E* x x F z <-> A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
41 40 albii 
 |-  ( A. z E* x x F z <-> A. z A. x A. y ( ( x F z /\ y F z ) -> x = y ) )
42 alrot3 
 |-  ( A. z A. x A. y ( ( x F z /\ y F z ) -> x = y ) <-> A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) )
43 41 42 bitri 
 |-  ( A. z E* x x F z <-> A. x A. y A. z ( ( x F z /\ y F z ) -> x = y ) )
44 r2al 
 |-  ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x A. y ( ( x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
45 38 43 44 3bitr4g 
 |-  ( F Fn A -> ( A. z E* x x F z <-> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
46 2 45 syl 
 |-  ( F : A --> B -> ( A. z E* x x F z <-> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
47 46 pm5.32i 
 |-  ( ( F : A --> B /\ A. z E* x x F z ) <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
48 1 47 bitri 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )