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

Theorem dff13 7270
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 6797 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧))
2 ffn 6728 . . . 4 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
3 vex 3466 . . . . . . . . . . . . . . 15 𝑥 ∈ V
4 vex 3466 . . . . . . . . . . . . . . 15 𝑧 ∈ V
53, 4breldm 5915 . . . . . . . . . . . . . 14 (𝑥𝐹𝑧𝑥 ∈ dom 𝐹)
6 fndm 6663 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
76eleq2d 2812 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹𝑥𝐴))
85, 7imbitrid 243 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑥𝐹𝑧𝑥𝐴))
9 vex 3466 . . . . . . . . . . . . . . 15 𝑦 ∈ V
109, 4breldm 5915 . . . . . . . . . . . . . 14 (𝑦𝐹𝑧𝑦 ∈ dom 𝐹)
116eleq2d 2812 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹𝑦𝐴))
1210, 11imbitrid 243 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑦𝐹𝑧𝑦𝐴))
138, 12anim12d 607 . . . . . . . . . . . 12 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) → (𝑥𝐴𝑦𝐴)))
1413pm4.71rd 561 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑥𝐹𝑧𝑦𝐹𝑧))))
15 eqcom 2733 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑧)
16 fnbrfvb 6954 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑧𝑥𝐹𝑧))
1715, 16bitrid 282 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑧 = (𝐹𝑥) ↔ 𝑥𝐹𝑧))
18 eqcom 2733 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑦) ↔ (𝐹𝑦) = 𝑧)
19 fnbrfvb 6954 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝐴𝑦𝐴) → ((𝐹𝑦) = 𝑧𝑦𝐹𝑧))
2018, 19bitrid 282 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐴𝑦𝐴) → (𝑧 = (𝐹𝑦) ↔ 𝑦𝐹𝑧))
2117, 20bi2anan9 636 . . . . . . . . . . . . 13 (((𝐹 Fn 𝐴𝑥𝐴) ∧ (𝐹 Fn 𝐴𝑦𝐴)) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) ↔ (𝑥𝐹𝑧𝑦𝐹𝑧)))
2221anandis 676 . . . . . . . . . . . 12 ((𝐹 Fn 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) ↔ (𝑥𝐹𝑧𝑦𝐹𝑧)))
2322pm5.32da 577 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑥𝐹𝑧𝑦𝐹𝑧))))
2414, 23bitr4d 281 . . . . . . . . . 10 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)))))
2524imbi1d 340 . . . . . . . . 9 (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ (((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) → 𝑥 = 𝑦)))
26 impexp 449 . . . . . . . . 9 ((((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
2725, 26bitrdi 286 . . . . . . . 8 (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))))
2827albidv 1916 . . . . . . 7 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))))
29 19.21v 1935 . . . . . . . 8 (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
30 19.23v 1938 . . . . . . . . . 10 (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))
31 fvex 6914 . . . . . . . . . . . 12 (𝐹𝑥) ∈ V
3231eqvinc 3634 . . . . . . . . . . 11 ((𝐹𝑥) = (𝐹𝑦) ↔ ∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)))
3332imbi1i 348 . . . . . . . . . 10 (((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))
3430, 33bitr4i 277 . . . . . . . . 9 (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
3534imbi2i 335 . . . . . . . 8 (((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3629, 35bitri 274 . . . . . . 7 (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3728, 36bitrdi 286 . . . . . 6 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
38372albidv 1919 . . . . 5 (𝐹 Fn 𝐴 → (∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
39 breq1 5156 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐹𝑧𝑦𝐹𝑧))
4039mo4 2555 . . . . . . 7 (∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4140albii 1814 . . . . . 6 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
42 alrot3 2150 . . . . . 6 (∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4341, 42bitri 274 . . . . 5 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
44 r2al 3185 . . . . 5 (∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
4538, 43, 443bitr4g 313 . . . 4 (𝐹 Fn 𝐴 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
462, 45syl 17 . . 3 (𝐹:𝐴𝐵 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
4746pm5.32i 573 . 2 ((𝐹:𝐴𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
481, 47bitri 274 1 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1532   = wceq 1534  wex 1774  wcel 2099  ∃*wmo 2527  wral 3051   class class class wbr 5153  dom cdm 5682   Fn wfn 6549  wf 6550  1-1wf1 6551  cfv 6554
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fv 6562
This theorem is referenced by:  dff13f  7271  f1veqaeq  7272  fpropnf1  7282  dff14a  7285  dff1o6  7289  fcof1  7301  nf1const  7317  soisoi  7340  f1opr  7481  f1o2ndf1  8136  fnwelem  8145  smo11  8394  tz7.48lem  8471  omsmo  8688  unxpdomlem3  9286  unfilem2  9345  fofinf1o  9374  inf3lem6  9676  r111  9818  fseqenlem1  10067  fodomacn  10099  alephf1  10128  alephiso  10141  ackbij1lem17  10279  infpssrlem5  10350  fin23lem28  10383  fin1a2lem2  10444  fin1a2lem4  10446  axcc2lem  10479  domtriomlem  10485  cnref1o  13021  injresinj  13808  om2uzf1oi  13973  cshf1  14818  wwlktovf1  14966  reeff1  16122  bitsf1  16446  crth  16780  eulerthlem2  16784  1arith  16929  vdwlem12  16994  xpsff1o  17582  setcmon  18109  fthestrcsetc  18174  embedsetcestrclem  18181  fthsetcestrc  18189  yoniso  18310  ghmf1  19240  kerf1ghm  19241  orbsta  19307  symgextf1  19419  symgfixf1  19435  odf1  19560  znf1o  21549  cygznlem3  21567  uvcf1  21790  lindff1  21818  mvrf1  21995  ply1sclf1  22280  scmatf1  22524  mdetunilem8  22612  mat2pmatf1  22722  pm2mpf1  22792  ist0-4  23724  ovolicc2lem4  25540  recosf1o  26562  efif1olem4  26572  basellem4  27112  mpodvdsmulf1o  27222  dvdsmulf1o  27224  lgsqrlem2  27376  lgseisenlem2  27405  2lgslem1b  27421  negsf1o  28063  om2noseqf1o  28275  axlowdimlem15  28890  upgrwlkdvdelem  29673  wlkswwlksf1o  29813  wwlksnextinj  29833  clwlkclwwlkf1  29943  clwwlkf1  29982  frgrncvvdeqlem8  30239  numclwwlk1lem2f1  30290  pjmf1  31649  unopf1o  31849  2ndresdju  32566  fnpreimac  32588  s3f1  32810  ccatf1  32812  swrdf1  32820  tocyccntz  33022  dff15  34921  f1resrcmplf1d  34924  f1resfz0f1d  34941  erdszelem9  35027  mrsubff1  35342  msubff1  35384  mvhf1  35387  f1omptsnlem  37043  fvineqsnf1  37117  fvineqsneu  37118  poimirlem26  37347  poimirlem27  37348  grpokerinj  37594  cdleme50f1  40242  dihf11  40966  hashscontpow  41820  hashnexinj  41826  aks6d1c5  41837  sticksstones2  41845  aks6d1c6lem3  41870  dnnumch3  42708  wessf1ornlem  44792  projf1o  44804  sumnnodd  45251  dvnprodlem1  45567  fourierdlem34  45762  fourierdlem51  45778  fsetsnf1  46667  cfsetsnfsetf1  46674  fcoresf1  46684  imasetpreimafvbijlemf1  46976  fargshiftf1  47013  sprsymrelf1  47068  prproropf1o  47079  fmtnof1  47107  prmdvdsfmtnof1  47159  uspgrsprf1  47524  1arymaptf1  48030  2arymaptf1  48041  rrx2xpref1o  48106
  Copyright terms: Public domain W3C validator