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

Theorem dff13 6152
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 5778 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  A. z E* x  x F z ) )
2 ffn 5729 . . . 4  |-  ( F : A --> B  ->  F  Fn  A )
3 vex 3116 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
4 vex 3116 . . . . . . . . . . . . . . 15  |-  z  e. 
_V
53, 4breldm 5205 . . . . . . . . . . . . . 14  |-  ( x F z  ->  x  e.  dom  F )
6 fndm 5678 . . . . . . . . . . . . . . 15  |-  ( F  Fn  A  ->  dom  F  =  A )
76eleq2d 2537 . . . . . . . . . . . . . 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 3116 . . . . . . . . . . . . . . 15  |-  y  e. 
_V
109, 4breldm 5205 . . . . . . . . . . . . . 14  |-  ( y F z  ->  y  e.  dom  F )
116eleq2d 2537 . . . . . . . . . . . . . 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 2476 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  x )  <->  ( F `  x )  =  z )
16 fnbrfvb 5906 . . . . . . . . . . . . . . 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 2476 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  y )  <->  ( F `  y )  =  z )
19 fnbrfvb 5906 . . . . . . . . . . . . . . 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 871 . . . . . . . . . . . . 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 828 . . . . . . . . . . . 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 1689 . . . . . . 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 1930 . . . . . . . 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 1932 . . . . . . . . . 10  |-  ( A. z ( ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )  <->  ( E. z ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )
)
31 fvex 5874 . . . . . . . . . . . 12  |-  ( F `
 x )  e. 
_V
3231eqvinc 3230 . . . . . . . . . . 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 1691 . . . . 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 4450 . . . . . . . 8  |-  ( x  =  y  ->  (
x F z  <->  y F
z ) )
4039mo4 2339 . . . . . . 7  |-  ( E* x  x F z  <->  A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y ) )
4140albii 1620 . . . . . 6  |-  ( A. z E* x  x F z  <->  A. z A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y )
)
42 alrot3 1795 . . . . . 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 2842 . . . . 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 1377    = wceq 1379   E.wex 1596    e. wcel 1767   E*wmo 2276   A.wral 2814   class class class wbr 4447   dom cdm 4999    Fn wfn 5581   -->wf 5582   -1-1->wf1 5583   ` cfv 5586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fv 5594
This theorem is referenced by:  dff13f  6153  f1veqaeq  6154  dff14a  6163  dff1o6  6167  fcof1  6176  soisoi  6210  f1o2ndf1  6888  fnwelem  6895  smo11  7032  tz7.48lem  7103  omsmo  7300  unxpdomlem3  7723  unfilem2  7781  fofinf1o  7797  inf3lem6  8046  r111  8189  fseqenlem1  8401  fodomacn  8433  alephf1  8462  alephiso  8475  ackbij1lem17  8612  infpssrlem5  8683  fin23lem28  8716  fin1a2lem2  8777  fin1a2lem4  8779  axcc2lem  8812  domtriomlem  8818  cnref1o  11211  injresinj  11890  om2uzf1oi  12028  wwlktovf1  12854  reeff1  13712  bitsf1  13951  crt  14163  eulerthlem2  14167  1arith  14300  vdwlem12  14365  xpsff1o  14819  setcmon  15268  yoniso  15408  ghmf1  16090  orbsta  16146  symgextf1  16241  symgfixf1  16258  odf1  16380  kerf1hrm  17175  mvrf1  17852  ply1sclf1  18101  znf1o  18357  cygznlem3  18375  uvcf1  18590  lindff1  18622  scmatf1  18800  mdetunilem8  18888  mat2pmatf1  18997  pm2mpf1  19067  ist0-4  19965  ovolicc2lem4  21666  recosf1o  22655  efif1olem4  22665  basellem4  23085  dvdsmulf1o  23198  lgsqrlem2  23345  lgseisenlem2  23353  axlowdimlem15  23935  wlkntrllem3  24239  wlkdvspthlem  24285  fargshiftf1  24313  constr3trllem2  24327  wlknwwlkninj  24387  wlkiswwlkinj  24394  wwlkextinj  24406  clwwlkf1  24472  clwlkf1clwwlk  24526  frgrancvvdeqlemB  24715  numclwlk1lem2f1  24771  pjmf1  26310  unopf1o  26511  erdszelem9  28283  ghomf1olem  28509  f1opr  29818  grpokerinj  29950  dnnumch3  30597  sumnnodd  31172  fourierdlem34  31441  fourierdlem51  31458  cdleme50f1  35339  dihf11  36064
  Copyright terms: Public domain W3C validator