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

Theorem dff13 6151
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 5770 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  A. z E* x  x F z ) )
2 ffn 5721 . . . 4  |-  ( F : A --> B  ->  F  Fn  A )
3 vex 3098 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
4 vex 3098 . . . . . . . . . . . . . . 15  |-  z  e. 
_V
53, 4breldm 5197 . . . . . . . . . . . . . 14  |-  ( x F z  ->  x  e.  dom  F )
6 fndm 5670 . . . . . . . . . . . . . . 15  |-  ( F  Fn  A  ->  dom  F  =  A )
76eleq2d 2513 . . . . . . . . . . . . . 14  |-  ( F  Fn  A  ->  (
x  e.  dom  F  <->  x  e.  A ) )
85, 7syl5ib 219 . . . . . . . . . . . . 13  |-  ( F  Fn  A  ->  (
x F z  ->  x  e.  A )
)
9 vex 3098 . . . . . . . . . . . . . . 15  |-  y  e. 
_V
109, 4breldm 5197 . . . . . . . . . . . . . 14  |-  ( y F z  ->  y  e.  dom  F )
116eleq2d 2513 . . . . . . . . . . . . . 14  |-  ( F  Fn  A  ->  (
y  e.  dom  F  <->  y  e.  A ) )
1210, 11syl5ib 219 . . . . . . . . . . . . 13  |-  ( F  Fn  A  ->  (
y F z  -> 
y  e.  A ) )
138, 12anim12d 563 . . . . . . . . . . . 12  |-  ( F  Fn  A  ->  (
( x F z  /\  y F z )  ->  ( x  e.  A  /\  y  e.  A ) ) )
1413pm4.71rd 635 . . . . . . . . . . 11  |-  ( F  Fn  A  ->  (
( x F z  /\  y F z )  <->  ( ( x  e.  A  /\  y  e.  A )  /\  (
x F z  /\  y F z ) ) ) )
15 eqcom 2452 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  x )  <->  ( F `  x )  =  z )
16 fnbrfvb 5898 . . . . . . . . . . . . . . 15  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( ( F `  x )  =  z  <-> 
x F z ) )
1715, 16syl5bb 257 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( z  =  ( F `  x )  <-> 
x F z ) )
18 eqcom 2452 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  y )  <->  ( F `  y )  =  z )
19 fnbrfvb 5898 . . . . . . . . . . . . . . 15  |-  ( ( F  Fn  A  /\  y  e.  A )  ->  ( ( F `  y )  =  z  <-> 
y F z ) )
2018, 19syl5bb 257 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  A  /\  y  e.  A )  ->  ( z  =  ( F `  y )  <-> 
y F z ) )
2117, 20bi2anan9 873 . . . . . . . . . . . . 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 830 . . . . . . . . . . . 12  |-  ( ( F  Fn  A  /\  ( x  e.  A  /\  y  e.  A
) )  ->  (
( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  <->  ( x F z  /\  y F z ) ) )
2322pm5.32da 641 . . . . . . . . . . 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 256 . . . . . . . . . 10  |-  ( F  Fn  A  ->  (
( x F z  /\  y F z )  <->  ( ( x  e.  A  /\  y  e.  A )  /\  (
z  =  ( F `
 x )  /\  z  =  ( F `  y ) ) ) ) )
2524imbi1d 317 . . . . . . . . 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 446 . . . . . . . . 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 261 . . . . . . . 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 1700 . . . . . . 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 1716 . . . . . . . 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 1747 . . . . . . . . . 10  |-  ( A. z ( ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )  <->  ( E. z ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )
)
31 fvex 5866 . . . . . . . . . . . 12  |-  ( F `
 x )  e. 
_V
3231eqvinc 3212 . . . . . . . . . . 11  |-  ( ( F `  x )  =  ( F `  y )  <->  E. z
( z  =  ( F `  x )  /\  z  =  ( F `  y ) ) )
3332imbi1i 325 . . . . . . . . . 10  |-  ( ( ( F `  x
)  =  ( F `
 y )  ->  x  =  y )  <->  ( E. z ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )
)
3430, 33bitr4i 252 . . . . . . . . 9  |-  ( A. z ( ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )  <->  ( ( F `  x
)  =  ( F `
 y )  ->  x  =  y )
)
3534imbi2i 312 . . . . . . . 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 249 . . . . . . 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 261 . . . . . 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 1702 . . . . 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 4440 . . . . . . . 8  |-  ( x  =  y  ->  (
x F z  <->  y F
z ) )
4039mo4 2323 . . . . . . 7  |-  ( E* x  x F z  <->  A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y ) )
4140albii 1627 . . . . . 6  |-  ( A. z E* x  x F z  <->  A. z A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y )
)
42 alrot3 1832 . . . . . 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 249 . . . . 5  |-  ( A. z E* x  x F z  <->  A. x A. y A. z ( ( x F z  /\  y F z )  ->  x  =  y )
)
44 r2al 2821 . . . . 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 288 . . . 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 16 . . 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 637 . 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 249 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 setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1381    = wceq 1383   E.wex 1599    e. wcel 1804   E*wmo 2269   A.wral 2793   class class class wbr 4437   dom cdm 4989    Fn wfn 5573   -->wf 5574   -1-1->wf1 5575   ` cfv 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fv 5586
This theorem is referenced by:  dff13f  6152  f1veqaeq  6153  dff14a  6162  dff1o6  6166  fcof1  6175  soisoi  6209  f1o2ndf1  6893  fnwelem  6900  smo11  7037  tz7.48lem  7108  omsmo  7305  unxpdomlem3  7728  unfilem2  7787  fofinf1o  7803  inf3lem6  8053  r111  8196  fseqenlem1  8408  fodomacn  8440  alephf1  8469  alephiso  8482  ackbij1lem17  8619  infpssrlem5  8690  fin23lem28  8723  fin1a2lem2  8784  fin1a2lem4  8786  axcc2lem  8819  domtriomlem  8825  cnref1o  11224  injresinj  11905  om2uzf1oi  12043  wwlktovf1  12874  reeff1  13732  bitsf1  13973  crt  14185  eulerthlem2  14189  1arith  14322  vdwlem12  14387  xpsff1o  14842  setcmon  15288  yoniso  15428  ghmf1  16169  orbsta  16225  symgextf1  16320  symgfixf1  16336  odf1  16458  kerf1hrm  17266  mvrf1  17955  ply1sclf1  18204  znf1o  18463  cygznlem3  18481  uvcf1  18696  lindff1  18728  scmatf1  18906  mdetunilem8  18994  mat2pmatf1  19103  pm2mpf1  19173  ist0-4  20103  ovolicc2lem4  21804  recosf1o  22794  efif1olem4  22804  basellem4  23229  dvdsmulf1o  23342  lgsqrlem2  23489  lgseisenlem2  23497  axlowdimlem15  24131  wlkntrllem3  24435  wlkdvspthlem  24481  fargshiftf1  24509  constr3trllem2  24523  wlknwwlkninj  24583  wlkiswwlkinj  24590  wwlkextinj  24602  clwwlkf1  24668  clwlkf1clwwlk  24722  frgrancvvdeqlemB  24910  numclwlk1lem2f1  24966  pjmf1  26506  unopf1o  26707  erdszelem9  28516  mrsubff1  28747  msubff1  28789  mvhf1  28792  ghomf1olem  28907  f1opr  30190  grpokerinj  30322  dnnumch3  30968  sumnnodd  31544  fourierdlem34  31812  fourierdlem51  31829  cdleme50f1  36009  dihf11  36734
  Copyright terms: Public domain W3C validator