MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dff13 Unicode version

Theorem dff13 5785
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.)
Assertion
Ref Expression
dff13  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  A. x  e.  A  A. y  e.  A  (
( F `  x
)  =  ( F `
 y )  ->  x  =  y )
) )
Distinct variable groups:    x, y, A    x, F, y
Allowed substitution hints:    B( x, y)

Proof of Theorem dff13
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 dff12 5438 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  A. z E* x  x F z ) )
2 ffn 5391 . . . 4  |-  ( F : A --> B  ->  F  Fn  A )
3 vex 2793 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
4 vex 2793 . . . . . . . . . . . . . . 15  |-  z  e. 
_V
53, 4breldm 4885 . . . . . . . . . . . . . 14  |-  ( x F z  ->  x  e.  dom  F )
6 fndm 5345 . . . . . . . . . . . . . . 15  |-  ( F  Fn  A  ->  dom  F  =  A )
76eleq2d 2352 . . . . . . . . . . . . . 14  |-  ( F  Fn  A  ->  (
x  e.  dom  F  <->  x  e.  A ) )
85, 7syl5ib 210 . . . . . . . . . . . . 13  |-  ( F  Fn  A  ->  (
x F z  ->  x  e.  A )
)
9 vex 2793 . . . . . . . . . . . . . . 15  |-  y  e. 
_V
109, 4breldm 4885 . . . . . . . . . . . . . 14  |-  ( y F z  ->  y  e.  dom  F )
116eleq2d 2352 . . . . . . . . . . . . . 14  |-  ( F  Fn  A  ->  (
y  e.  dom  F  <->  y  e.  A ) )
1210, 11syl5ib 210 . . . . . . . . . . . . 13  |-  ( F  Fn  A  ->  (
y F z  -> 
y  e.  A ) )
138, 12anim12d 546 . . . . . . . . . . . 12  |-  ( F  Fn  A  ->  (
( x F z  /\  y F z )  ->  ( x  e.  A  /\  y  e.  A ) ) )
1413pm4.71rd 616 . . . . . . . . . . 11  |-  ( F  Fn  A  ->  (
( x F z  /\  y F z )  <->  ( ( x  e.  A  /\  y  e.  A )  /\  (
x F z  /\  y F z ) ) ) )
15 eqcom 2287 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  x )  <->  ( F `  x )  =  z )
16 fnbrfvb 5565 . . . . . . . . . . . . . . 15  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( ( F `  x )  =  z  <-> 
x F z ) )
1715, 16syl5bb 248 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( z  =  ( F `  x )  <-> 
x F z ) )
18 eqcom 2287 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  y )  <->  ( F `  y )  =  z )
19 fnbrfvb 5565 . . . . . . . . . . . . . . 15  |-  ( ( F  Fn  A  /\  y  e.  A )  ->  ( ( F `  y )  =  z  <-> 
y F z ) )
2018, 19syl5bb 248 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  A  /\  y  e.  A )  ->  ( z  =  ( F `  y )  <-> 
y F z ) )
2117, 20bi2anan9 843 . . . . . . . . . . . . 13  |-  ( ( ( F  Fn  A  /\  x  e.  A
)  /\  ( F  Fn  A  /\  y  e.  A ) )  -> 
( ( z  =  ( F `  x
)  /\  z  =  ( F `  y ) )  <->  ( x F z  /\  y F z ) ) )
2221anandis 803 . . . . . . . . . . . 12  |-  ( ( F  Fn  A  /\  ( x  e.  A  /\  y  e.  A
) )  ->  (
( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  <->  ( x F z  /\  y F z ) ) )
2322pm5.32da 622 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
2414, 23bitr4d 247 . . . . . . . . . 10  |-  ( F  Fn  A  ->  (
( x F z  /\  y F z )  <->  ( ( x  e.  A  /\  y  e.  A )  /\  (
z  =  ( F `
 x )  /\  z  =  ( F `  y ) ) ) ) )
2524imbi1d 308 . . . . . . . . 9  |-  ( 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 433 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
2725, 26syl6bb 252 . . . . . . . 8  |-  ( 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 ) ) ) )
2827albidv 1613 . . . . . . 7  |-  ( 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 1833 . . . . . . . 8  |-  ( 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 1834 . . . . . . . . . 10  |-  ( A. z ( ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )  <->  ( E. z ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )
)
31 fvex 5541 . . . . . . . . . . . 12  |-  ( F `
 x )  e. 
_V
3231eqvinc 2897 . . . . . . . . . . 11  |-  ( ( F `  x )  =  ( F `  y )  <->  E. z
( z  =  ( F `  x )  /\  z  =  ( F `  y ) ) )
3332imbi1i 315 . . . . . . . . . 10  |-  ( ( ( F `  x
)  =  ( F `
 y )  ->  x  =  y )  <->  ( E. z ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )
)
3430, 33bitr4i 243 . . . . . . . . 9  |-  ( A. z ( ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )  <->  ( ( F `  x
)  =  ( F `
 y )  ->  x  =  y )
)
3534imbi2i 303 . . . . . . . 8  |-  ( ( ( 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 ) ) )
3629, 35bitri 240 . . . . . . 7  |-  ( 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 ) ) )
3728, 36syl6bb 252 . . . . . 6  |-  ( 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 ) ) ) )
38372albidv 1615 . . . . 5  |-  ( 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 4028 . . . . . . . 8  |-  ( x  =  y  ->  (
x F z  <->  y F
z ) )
4039mo4 2178 . . . . . . 7  |-  ( E* x  x F z  <->  A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y ) )
4140albii 1555 . . . . . 6  |-  ( A. z E* x  x F z  <->  A. z A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y )
)
42 alrot3 1714 . . . . . 6  |-  ( 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 ) )
4341, 42bitri 240 . . . . 5  |-  ( A. z E* x  x F z  <->  A. x A. y A. z ( ( x F z  /\  y F z )  ->  x  =  y )
)
44 r2al 2582 . . . . 5  |-  ( 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 ) ) )
4538, 43, 443bitr4g 279 . . . 4  |-  ( F  Fn  A  ->  ( A. z E* x  x F z  <->  A. x  e.  A  A. y  e.  A  ( ( F `  x )  =  ( F `  y )  ->  x  =  y ) ) )
462, 45syl 15 . . 3  |-  ( F : A --> B  -> 
( A. z E* x  x F z  <->  A. x  e.  A  A. y  e.  A  ( ( F `  x )  =  ( F `  y )  ->  x  =  y ) ) )
4746pm5.32i 618 . 2  |-  ( ( 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 )
) )
481, 47bitri 240 1  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  A. x  e.  A  A. y  e.  A  (
( F `  x
)  =  ( F `
 y )  ->  x  =  y )
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1529   E.wex 1530    = wceq 1625    e. wcel 1686   E*wmo 2146   A.wral 2545   class class class wbr 4025   dom cdm 4691    Fn wfn 5252   -->wf 5253   -1-1->wf1 5254   ` cfv 5257
This theorem is referenced by:  dff13f  5786  f1fveq  5788  dff1o6  5793  fcof1  5799  soisoi  5827  fnwelem  6232  smo11  6383  tz7.48lem  6455  omsmo  6654  unxpdomlem3  7071  unfilem2  7124  fofinf1o  7139  inf3lem6  7336  r111  7449  fseqenlem1  7653  fodomacn  7685  alephf1  7714  alephiso  7727  ackbij1lem17  7864  infpssrlem5  7935  fin23lem28  7968  fin1a2lem2  8029  fin1a2lem4  8031  axcc2lem  8064  domtriomlem  8070  cnref1o  10351  om2uzf1oi  11018  reeff1  12402  bitsf1  12639  crt  12848  eulerthlem2  12852  1arith  12976  vdwlem12  13041  xpsff1o  13472  setcmon  13921  yoniso  14061  ghmf1  14713  orbsta  14769  odf1  14877  mvrf1  16172  ply1sclf1  16366  znf1o  16507  cygznlem3  16525  ist0-4  17422  ovolicc2lem4  18881  recosf1o  19899  efif1olem4  19909  basellem4  20323  dvdsmulf1o  20436  lgsqrlem2  20583  lgseisenlem2  20591  pjmf1  22297  unopf1o  22498  erdszelem9  23732  ghomf1olem  24003  axlowdimlem15  24586  injsurinj  25160  trnij  25626  f1opr  26402  grpokerinj  26586  dnnumch3  27155  uvcf1  27252  lindff1  27301  cdleme50f1  30805  dihf11  31530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-id 4311  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fv 5265
  Copyright terms: Public domain W3C validator