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 syl5ib
 |-  ( 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 syl5ib
 |-  ( 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 ) ) )