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

Theorem dff13 5783
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 5436 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  A. z E* x  x F z ) )
2 ffn 5389 . . . 4  |-  ( F : A --> B  ->  F  Fn  A )
3 vex 2791 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
4 vex 2791 . . . . . . . . . . . . . . 15  |-  z  e. 
_V
53, 4breldm 4883 . . . . . . . . . . . . . 14  |-  ( x F z  ->  x  e.  dom  F )
6 fndm 5343 . . . . . . . . . . . . . . 15  |-  ( F  Fn  A  ->  dom  F  =  A )
76eleq2d 2350 . . . . . . . . . . . . . 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 2791 . . . . . . . . . . . . . . 15  |-  y  e. 
_V
109, 4breldm 4883 . . . . . . . . . . . . . 14  |-  ( y F z  ->  y  e.  dom  F )
116eleq2d 2350 . . . . . . . . . . . . . 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 2285 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  x )  <->  ( F `  x )  =  z )
16 fnbrfvb 5563 . . . . . . . . . . . . . . 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 2285 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  y )  <->  ( F `  y )  =  z )
19 fnbrfvb 5563 . . . . . . . . . . . . . . 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 1611 . . . . . . 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 1831 . . . . . . . 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 1832 . . . . . . . . . 10  |-  ( A. z ( ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )  <->  ( E. z ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )
)
31 fvex 5539 . . . . . . . . . . . 12  |-  ( F `
 x )  e. 
_V
3231eqvinc 2895 . . . . . . . . . . 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 1613 . . . . 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 4026 . . . . . . . 8  |-  ( x  =  y  ->  (
x F z  <->  y F
z ) )
4039mo4 2176 . . . . . . 7  |-  ( E* x  x F z  <->  A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y ) )
4140albii 1553 . . . . . 6  |-  ( A. z E* x  x F z  <->  A. z A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y )
)
42 alrot3 1712 . . . . . 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 2580 . . . . 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 1527   E.wex 1528    = wceq 1623    e. wcel 1684   E*wmo 2144   A.wral 2543   class class class wbr 4023   dom cdm 4689    Fn wfn 5250   -->wf 5251   -1-1->wf1 5252   ` cfv 5255
This theorem is referenced by:  dff13f  5784  f1fveq  5786  dff1o6  5791  fcof1  5797  soisoi  5825  fnwelem  6230  smo11  6381  tz7.48lem  6453  omsmo  6652  unxpdomlem3  7069  unfilem2  7122  fofinf1o  7137  inf3lem6  7334  r111  7447  fseqenlem1  7651  fodomacn  7683  alephf1  7712  alephiso  7725  ackbij1lem17  7862  infpssrlem5  7933  fin23lem28  7966  fin1a2lem2  8027  fin1a2lem4  8029  axcc2lem  8062  domtriomlem  8068  cnref1o  10349  om2uzf1oi  11016  reeff1  12400  bitsf1  12637  crt  12846  eulerthlem2  12850  1arith  12974  vdwlem12  13039  xpsff1o  13470  setcmon  13919  yoniso  14059  ghmf1  14711  orbsta  14767  odf1  14875  mvrf1  16170  ply1sclf1  16364  znf1o  16505  cygznlem3  16523  ist0-4  17420  ovolicc2lem4  18879  recosf1o  19897  efif1olem4  19907  basellem4  20321  dvdsmulf1o  20434  lgsqrlem2  20581  lgseisenlem2  20589  pjmf1  22295  unopf1o  22496  erdszelem9  23730  ghomf1olem  24001  axlowdimlem15  24584  injsurinj  25149  trnij  25615  f1opr  26391  grpokerinj  26575  dnnumch3  27144  uvcf1  27241  lindff1  27290  cdleme50f1  30732  dihf11  31457
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fv 5263
  Copyright terms: Public domain W3C validator