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

Theorem dff13 5635
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
StepHypRef Expression
1 dff12 5293 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  A. z E* x  x F z ) )
2 ffn 5246 . . . 4  |-  ( F : A --> B  ->  F  Fn  A )
3 vex 2730 . . . . . . . . . . . . . . 15  |-  x  e. 
_V
4 vex 2730 . . . . . . . . . . . . . . 15  |-  z  e. 
_V
53, 4breldm 4790 . . . . . . . . . . . . . 14  |-  ( x F z  ->  x  e.  dom  F )
6 fndm 5200 . . . . . . . . . . . . . . 15  |-  ( F  Fn  A  ->  dom  F  =  A )
76eleq2d 2320 . . . . . . . . . . . . . 14  |-  ( F  Fn  A  ->  (
x  e.  dom  F  <->  x  e.  A ) )
85, 7syl5ib 212 . . . . . . . . . . . . 13  |-  ( F  Fn  A  ->  (
x F z  ->  x  e.  A )
)
9 vex 2730 . . . . . . . . . . . . . . 15  |-  y  e. 
_V
109, 4breldm 4790 . . . . . . . . . . . . . 14  |-  ( y F z  ->  y  e.  dom  F )
116eleq2d 2320 . . . . . . . . . . . . . 14  |-  ( F  Fn  A  ->  (
y  e.  dom  F  <->  y  e.  A ) )
1210, 11syl5ib 212 . . . . . . . . . . . . 13  |-  ( F  Fn  A  ->  (
y F z  -> 
y  e.  A ) )
138, 12anim12d 548 . . . . . . . . . . . 12  |-  ( F  Fn  A  ->  (
( x F z  /\  y F z )  ->  ( x  e.  A  /\  y  e.  A ) ) )
1413pm4.71rd 619 . . . . . . . . . . 11  |-  ( F  Fn  A  ->  (
( x F z  /\  y F z )  <->  ( ( x  e.  A  /\  y  e.  A )  /\  (
x F z  /\  y F z ) ) ) )
15 eqcom 2255 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  x )  <->  ( F `  x )  =  z )
16 fnbrfvb 5415 . . . . . . . . . . . . . . 15  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( ( F `  x )  =  z  <-> 
x F z ) )
1715, 16syl5bb 250 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( z  =  ( F `  x )  <-> 
x F z ) )
18 eqcom 2255 . . . . . . . . . . . . . . 15  |-  ( z  =  ( F `  y )  <->  ( F `  y )  =  z )
19 fnbrfvb 5415 . . . . . . . . . . . . . . 15  |-  ( ( F  Fn  A  /\  y  e.  A )  ->  ( ( F `  y )  =  z  <-> 
y F z ) )
2018, 19syl5bb 250 . . . . . . . . . . . . . 14  |-  ( ( F  Fn  A  /\  y  e.  A )  ->  ( z  =  ( F `  y )  <-> 
y F z ) )
2117, 20bi2anan9 848 . . . . . . . . . . . . 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 806 . . . . . . . . . . . 12  |-  ( ( F  Fn  A  /\  ( x  e.  A  /\  y  e.  A
) )  ->  (
( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  <->  ( x F z  /\  y F z ) ) )
2322pm5.32da 625 . . . . . . . . . . 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 249 . . . . . . . . . 10  |-  ( F  Fn  A  ->  (
( x F z  /\  y F z )  <->  ( ( x  e.  A  /\  y  e.  A )  /\  (
z  =  ( F `
 x )  /\  z  =  ( F `  y ) ) ) ) )
2524imbi1d 310 . . . . . . . . 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 435 . . . . . . . . 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 254 . . . . . . . 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 2004 . . . . . . 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 2011 . . . . . . . 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 2021 . . . . . . . . . 10  |-  ( A. z ( ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )  <->  ( E. z ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )
)
31 fvex 5391 . . . . . . . . . . . 12  |-  ( F `
 x )  e. 
_V
3231eqvinc 2832 . . . . . . . . . . 11  |-  ( ( F `  x )  =  ( F `  y )  <->  E. z
( z  =  ( F `  x )  /\  z  =  ( F `  y ) ) )
3332imbi1i 317 . . . . . . . . . 10  |-  ( ( ( F `  x
)  =  ( F `
 y )  ->  x  =  y )  <->  ( E. z ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )
)
3430, 33bitr4i 245 . . . . . . . . 9  |-  ( A. z ( ( z  =  ( F `  x )  /\  z  =  ( F `  y ) )  ->  x  =  y )  <->  ( ( F `  x
)  =  ( F `
 y )  ->  x  =  y )
)
3534imbi2i 305 . . . . . . . 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 242 . . . . . . 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 254 . . . . . 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 2006 . . . . 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 3923 . . . . . . . 8  |-  ( x  =  y  ->  (
x F z  <->  y F
z ) )
4039mo4 2146 . . . . . . 7  |-  ( E* x  x F z  <->  A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y ) )
4140albii 1554 . . . . . 6  |-  ( A. z E* x  x F z  <->  A. z A. x A. y ( ( x F z  /\  y F z )  ->  x  =  y )
)
42 alrot3 1610 . . . . . 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 242 . . . . 5  |-  ( A. z E* x  x F z  <->  A. x A. y A. z ( ( x F z  /\  y F z )  ->  x  =  y )
)
44 r2al 2542 . . . . 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 281 . . . 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 17 . . 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 621 . 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 242 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 6    <-> wb 178    /\ wa 360   A.wal 1532   E.wex 1537    = wceq 1619    e. wcel 1621   E*wmo 2115   A.wral 2509   class class class wbr 3920   dom cdm 4580    Fn wfn 4587   -->wf 4588   -1-1->wf1 4589   ` cfv 4592
This theorem is referenced by:  dff13f  5636  f1fveq  5638  dff1o6  5643  fcof1  5649  soisoi  5677  fnwelem  6082  smo11  6267  tz7.48lem  6339  omsmo  6538  unxpdomlem3  6954  unfilem2  7007  fofinf1o  7022  inf3lem6  7218  r111  7331  fseqenlem1  7535  fodomacn  7567  alephf1  7596  alephiso  7609  ackbij1lem17  7746  infpssrlem5  7817  fin23lem28  7850  fin1a2lem2  7911  fin1a2lem4  7913  axcc2lem  7946  domtriomlem  7952  cnref1o  10228  om2uzf1oi  10894  reeff1  12274  bitsf1  12511  crt  12720  eulerthlem2  12724  1arith  12848  vdwlem12  12913  xpsff1o  13344  setcmon  13763  yoniso  13903  ghmf1  14546  orbsta  14602  odf1  14710  mvrf1  16002  ply1sclf1  16196  znf1o  16337  cygznlem3  16355  ist0-4  17252  ovolicc2lem4  18711  recosf1o  19729  efif1olem4  19739  basellem4  20153  dvdsmulf1o  20266  lgsqrlem2  20413  lgseisenlem2  20421  pjmf1  22143  unopf1o  22326  erdszelem9  22901  ghomf1olem  23172  axlowdimlem15  23758  injsurinj  24315  trnij  24781  f1opr  25557  grpokerinj  25741  dnnumch3  26310  uvcf1  26407  lindff1  26456  cdleme50f1  29421  dihf11  30146
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108  ax-un 4403
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-sbc 2922  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-id 4202  df-xp 4594  df-rel 4595  df-cnv 4596  df-co 4597  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fun 4602  df-fn 4603  df-f 4604  df-f1 4605  df-fv 4608
  Copyright terms: Public domain W3C validator