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

Theorem dff13 7275
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 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐹,𝑦
Allowed substitution hints:   𝐵(𝑥,𝑦)

Proof of Theorem dff13
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 dff12 6803 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧))
2 ffn 6736 . . . 4 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
3 vex 3484 . . . . . . . . . . . . . . 15 𝑥 ∈ V
4 vex 3484 . . . . . . . . . . . . . . 15 𝑧 ∈ V
53, 4breldm 5919 . . . . . . . . . . . . . 14 (𝑥𝐹𝑧𝑥 ∈ dom 𝐹)
6 fndm 6671 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
76eleq2d 2827 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹𝑥𝐴))
85, 7imbitrid 244 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑥𝐹𝑧𝑥𝐴))
9 vex 3484 . . . . . . . . . . . . . . 15 𝑦 ∈ V
109, 4breldm 5919 . . . . . . . . . . . . . 14 (𝑦𝐹𝑧𝑦 ∈ dom 𝐹)
116eleq2d 2827 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹𝑦𝐴))
1210, 11imbitrid 244 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑦𝐹𝑧𝑦𝐴))
138, 12anim12d 609 . . . . . . . . . . . 12 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) → (𝑥𝐴𝑦𝐴)))
1413pm4.71rd 562 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑥𝐹𝑧𝑦𝐹𝑧))))
15 eqcom 2744 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑧)
16 fnbrfvb 6959 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑧𝑥𝐹𝑧))
1715, 16bitrid 283 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑧 = (𝐹𝑥) ↔ 𝑥𝐹𝑧))
18 eqcom 2744 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑦) ↔ (𝐹𝑦) = 𝑧)
19 fnbrfvb 6959 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝐴𝑦𝐴) → ((𝐹𝑦) = 𝑧𝑦𝐹𝑧))
2018, 19bitrid 283 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐴𝑦𝐴) → (𝑧 = (𝐹𝑦) ↔ 𝑦𝐹𝑧))
2117, 20bi2anan9 638 . . . . . . . . . . . . 13 (((𝐹 Fn 𝐴𝑥𝐴) ∧ (𝐹 Fn 𝐴𝑦𝐴)) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) ↔ (𝑥𝐹𝑧𝑦𝐹𝑧)))
2221anandis 678 . . . . . . . . . . . 12 ((𝐹 Fn 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) ↔ (𝑥𝐹𝑧𝑦𝐹𝑧)))
2322pm5.32da 579 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑥𝐹𝑧𝑦𝐹𝑧))))
2414, 23bitr4d 282 . . . . . . . . . 10 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)))))
2524imbi1d 341 . . . . . . . . 9 (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ (((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) → 𝑥 = 𝑦)))
26 impexp 450 . . . . . . . . 9 ((((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
2725, 26bitrdi 287 . . . . . . . 8 (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))))
2827albidv 1920 . . . . . . 7 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))))
29 19.21v 1939 . . . . . . . 8 (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
30 19.23v 1942 . . . . . . . . . 10 (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))
31 fvex 6919 . . . . . . . . . . . 12 (𝐹𝑥) ∈ V
3231eqvinc 3649 . . . . . . . . . . 11 ((𝐹𝑥) = (𝐹𝑦) ↔ ∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)))
3332imbi1i 349 . . . . . . . . . 10 (((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))
3430, 33bitr4i 278 . . . . . . . . 9 (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
3534imbi2i 336 . . . . . . . 8 (((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3629, 35bitri 275 . . . . . . 7 (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3728, 36bitrdi 287 . . . . . 6 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
38372albidv 1923 . . . . 5 (𝐹 Fn 𝐴 → (∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
39 breq1 5146 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐹𝑧𝑦𝐹𝑧))
4039mo4 2566 . . . . . . 7 (∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4140albii 1819 . . . . . 6 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
42 alrot3 2160 . . . . . 6 (∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4341, 42bitri 275 . . . . 5 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
44 r2al 3195 . . . . 5 (∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
4538, 43, 443bitr4g 314 . . . 4 (𝐹 Fn 𝐴 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
462, 45syl 17 . . 3 (𝐹:𝐴𝐵 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
4746pm5.32i 574 . 2 ((𝐹:𝐴𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
481, 47bitri 275 1 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538   = wceq 1540  wex 1779  wcel 2108  ∃*wmo 2538  wral 3061   class class class wbr 5143  dom cdm 5685   Fn wfn 6556  wf 6557  1-1wf1 6558  cfv 6561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fv 6569
This theorem is referenced by:  dff13f  7276  f1veqaeq  7277  fpropnf1  7287  dff14a  7290  dff1o6  7295  fcof1  7307  nf1const  7324  soisoi  7348  f1opr  7489  f1o2ndf1  8147  fnwelem  8156  smo11  8404  tz7.48lem  8481  omsmo  8696  unxpdomlem3  9288  unfilem2  9344  fofinf1o  9372  inf3lem6  9673  r111  9815  fseqenlem1  10064  fodomacn  10096  alephf1  10125  alephiso  10138  ackbij1lem17  10275  infpssrlem5  10347  fin23lem28  10380  fin1a2lem2  10441  fin1a2lem4  10443  axcc2lem  10476  domtriomlem  10482  cnref1o  13027  injresinj  13827  om2uzf1oi  13994  cshf1  14848  wwlktovf1  14996  reeff1  16156  bitsf1  16483  crth  16815  eulerthlem2  16819  1arith  16965  vdwlem12  17030  xpsff1o  17612  setcmon  18132  fthestrcsetc  18195  embedsetcestrclem  18202  fthsetcestrc  18210  yoniso  18330  ghmf1  19264  kerf1ghm  19265  orbsta  19331  symgextf1  19439  symgfixf1  19455  odf1  19580  znf1o  21570  cygznlem3  21588  uvcf1  21812  lindff1  21840  mvrf1  22006  ply1sclf1  22292  scmatf1  22537  mdetunilem8  22625  mat2pmatf1  22735  pm2mpf1  22805  ist0-4  23737  ovolicc2lem4  25555  recosf1o  26577  efif1olem4  26587  basellem4  27127  mpodvdsmulf1o  27237  dvdsmulf1o  27239  lgsqrlem2  27391  lgseisenlem2  27420  2lgslem1b  27436  negsf1o  28086  om2noseqf1o  28307  axlowdimlem15  28971  upgrwlkdvdelem  29756  wlkswwlksf1o  29899  wwlksnextinj  29919  clwlkclwwlkf1  30029  clwwlkf1  30068  frgrncvvdeqlem8  30325  numclwwlk1lem2f1  30376  pjmf1  31735  unopf1o  31935  2ndresdju  32659  fnpreimac  32681  s3f1  32931  ccatf1  32933  swrdf1  32941  mndlactf1  33031  mndractf1  33033  tocyccntz  33164  dff15  35098  f1resrcmplf1d  35101  f1resfz0f1d  35119  erdszelem9  35204  mrsubff1  35519  msubff1  35561  mvhf1  35564  f1omptsnlem  37337  fvineqsnf1  37411  fvineqsneu  37412  poimirlem26  37653  poimirlem27  37654  grpokerinj  37900  cdleme50f1  40545  dihf11  41269  hashscontpow  42123  hashnexinj  42129  aks6d1c5  42140  sticksstones2  42148  aks6d1c6lem3  42173  fimgmcyc  42544  dnnumch3  43059  wessf1ornlem  45190  projf1o  45202  sumnnodd  45645  dvnprodlem1  45961  fourierdlem34  46156  fourierdlem51  46172  fsetsnf1  47064  cfsetsnfsetf1  47071  fcoresf1  47081  imasetpreimafvbijlemf1  47391  fargshiftf1  47428  sprsymrelf1  47483  prproropf1o  47494  fmtnof1  47522  prmdvdsfmtnof1  47574  uspgrsprf1  48063  1arymaptf1  48563  2arymaptf1  48574  rrx2xpref1o  48639
  Copyright terms: Public domain W3C validator