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

Theorem dff13 7274
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 3481 . . . . . . . . . . . . . . 15 𝑥 ∈ V
4 vex 3481 . . . . . . . . . . . . . . 15 𝑧 ∈ V
53, 4breldm 5921 . . . . . . . . . . . . . 14 (𝑥𝐹𝑧𝑥 ∈ dom 𝐹)
6 fndm 6671 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
76eleq2d 2824 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹𝑥𝐴))
85, 7imbitrid 244 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑥𝐹𝑧𝑥𝐴))
9 vex 3481 . . . . . . . . . . . . . . 15 𝑦 ∈ V
109, 4breldm 5921 . . . . . . . . . . . . . 14 (𝑦𝐹𝑧𝑦 ∈ dom 𝐹)
116eleq2d 2824 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹𝑦𝐴))
1210, 11imbitrid 244 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑦𝐹𝑧𝑦𝐴))
138, 12anim12d 609 . . . . . . . . . . . 12 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) → (𝑥𝐴𝑦𝐴)))
1413pm4.71rd 562 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑥𝐹𝑧𝑦𝐹𝑧))))
15 eqcom 2741 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑧)
16 fnbrfvb 6959 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑧𝑥𝐹𝑧))
1715, 16bitrid 283 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑧 = (𝐹𝑥) ↔ 𝑥𝐹𝑧))
18 eqcom 2741 . . . . . . . . . . . . . . 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 1917 . . . . . . 7 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))))
29 19.21v 1936 . . . . . . . 8 (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
30 19.23v 1939 . . . . . . . . . 10 (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))
31 fvex 6919 . . . . . . . . . . . 12 (𝐹𝑥) ∈ V
3231eqvinc 3648 . . . . . . . . . . 11 ((𝐹𝑥) = (𝐹𝑦) ↔ ∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)))
3332imbi1i 349 . . . . . . . . . 10 (((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))
3430, 33bitr4i 278 . . . . . . . . 9 (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
3534imbi2i 336 . . . . . . . 8 (((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3629, 35bitri 275 . . . . . . 7 (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3728, 36bitrdi 287 . . . . . 6 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
38372albidv 1920 . . . . 5 (𝐹 Fn 𝐴 → (∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
39 breq1 5150 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐹𝑧𝑦𝐹𝑧))
4039mo4 2563 . . . . . . 7 (∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4140albii 1815 . . . . . 6 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
42 alrot3 2157 . . . . . 6 (∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4341, 42bitri 275 . . . . 5 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
44 r2al 3192 . . . . 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 1534   = wceq 1536  wex 1775  wcel 2105  ∃*wmo 2535  wral 3058   class class class wbr 5147  dom cdm 5688   Fn wfn 6557  wf 6558  1-1wf1 6559  cfv 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fv 6570
This theorem is referenced by:  dff13f  7275  f1veqaeq  7276  fpropnf1  7286  dff14a  7289  dff1o6  7294  fcof1  7306  nf1const  7323  soisoi  7347  f1opr  7488  f1o2ndf1  8145  fnwelem  8154  smo11  8402  tz7.48lem  8479  omsmo  8694  unxpdomlem3  9285  unfilem2  9341  fofinf1o  9369  inf3lem6  9670  r111  9812  fseqenlem1  10061  fodomacn  10093  alephf1  10122  alephiso  10135  ackbij1lem17  10272  infpssrlem5  10344  fin23lem28  10377  fin1a2lem2  10438  fin1a2lem4  10440  axcc2lem  10473  domtriomlem  10479  cnref1o  13024  injresinj  13823  om2uzf1oi  13990  cshf1  14844  wwlktovf1  14992  reeff1  16152  bitsf1  16479  crth  16811  eulerthlem2  16815  1arith  16960  vdwlem12  17025  xpsff1o  17613  setcmon  18140  fthestrcsetc  18205  embedsetcestrclem  18212  fthsetcestrc  18220  yoniso  18341  ghmf1  19276  kerf1ghm  19277  orbsta  19343  symgextf1  19453  symgfixf1  19469  odf1  19594  znf1o  21587  cygznlem3  21605  uvcf1  21829  lindff1  21857  mvrf1  22023  ply1sclf1  22307  scmatf1  22552  mdetunilem8  22640  mat2pmatf1  22750  pm2mpf1  22820  ist0-4  23752  ovolicc2lem4  25568  recosf1o  26591  efif1olem4  26601  basellem4  27141  mpodvdsmulf1o  27251  dvdsmulf1o  27253  lgsqrlem2  27405  lgseisenlem2  27434  2lgslem1b  27450  negsf1o  28100  om2noseqf1o  28321  axlowdimlem15  28985  upgrwlkdvdelem  29768  wlkswwlksf1o  29908  wwlksnextinj  29928  clwlkclwwlkf1  30038  clwwlkf1  30077  frgrncvvdeqlem8  30334  numclwwlk1lem2f1  30385  pjmf1  31744  unopf1o  31944  2ndresdju  32665  fnpreimac  32687  s3f1  32915  ccatf1  32917  swrdf1  32925  mndlactf1  33013  mndractf1  33015  tocyccntz  33146  dff15  35076  f1resrcmplf1d  35079  f1resfz0f1d  35097  erdszelem9  35183  mrsubff1  35498  msubff1  35540  mvhf1  35543  f1omptsnlem  37318  fvineqsnf1  37392  fvineqsneu  37393  poimirlem26  37632  poimirlem27  37633  grpokerinj  37879  cdleme50f1  40525  dihf11  41249  hashscontpow  42103  hashnexinj  42109  aks6d1c5  42120  sticksstones2  42128  aks6d1c6lem3  42153  fimgmcyc  42520  dnnumch3  43035  wessf1ornlem  45127  projf1o  45139  sumnnodd  45585  dvnprodlem1  45901  fourierdlem34  46096  fourierdlem51  46112  fsetsnf1  47001  cfsetsnfsetf1  47008  fcoresf1  47018  imasetpreimafvbijlemf1  47328  fargshiftf1  47365  sprsymrelf1  47420  prproropf1o  47431  fmtnof1  47459  prmdvdsfmtnof1  47511  uspgrsprf1  47990  1arymaptf1  48491  2arymaptf1  48502  rrx2xpref1o  48567
  Copyright terms: Public domain W3C validator