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

Theorem dff13 6878
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 6442 . 2 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧))
2 ffn 6382 . . . 4 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
3 vex 3440 . . . . . . . . . . . . . . 15 𝑥 ∈ V
4 vex 3440 . . . . . . . . . . . . . . 15 𝑧 ∈ V
53, 4breldm 5663 . . . . . . . . . . . . . 14 (𝑥𝐹𝑧𝑥 ∈ dom 𝐹)
6 fndm 6325 . . . . . . . . . . . . . . 15 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
76eleq2d 2868 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑥 ∈ dom 𝐹𝑥𝐴))
85, 7syl5ib 245 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑥𝐹𝑧𝑥𝐴))
9 vex 3440 . . . . . . . . . . . . . . 15 𝑦 ∈ V
109, 4breldm 5663 . . . . . . . . . . . . . 14 (𝑦𝐹𝑧𝑦 ∈ dom 𝐹)
116eleq2d 2868 . . . . . . . . . . . . . 14 (𝐹 Fn 𝐴 → (𝑦 ∈ dom 𝐹𝑦𝐴))
1210, 11syl5ib 245 . . . . . . . . . . . . 13 (𝐹 Fn 𝐴 → (𝑦𝐹𝑧𝑦𝐴))
138, 12anim12d 608 . . . . . . . . . . . 12 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) → (𝑥𝐴𝑦𝐴)))
1413pm4.71rd 563 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑥𝐹𝑧𝑦𝐹𝑧))))
15 eqcom 2802 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑧)
16 fnbrfvb 6586 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑧𝑥𝐹𝑧))
1715, 16syl5bb 284 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑧 = (𝐹𝑥) ↔ 𝑥𝐹𝑧))
18 eqcom 2802 . . . . . . . . . . . . . . 15 (𝑧 = (𝐹𝑦) ↔ (𝐹𝑦) = 𝑧)
19 fnbrfvb 6586 . . . . . . . . . . . . . . 15 ((𝐹 Fn 𝐴𝑦𝐴) → ((𝐹𝑦) = 𝑧𝑦𝐹𝑧))
2018, 19syl5bb 284 . . . . . . . . . . . . . 14 ((𝐹 Fn 𝐴𝑦𝐴) → (𝑧 = (𝐹𝑦) ↔ 𝑦𝐹𝑧))
2117, 20bi2anan9 635 . . . . . . . . . . . . 13 (((𝐹 Fn 𝐴𝑥𝐴) ∧ (𝐹 Fn 𝐴𝑦𝐴)) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) ↔ (𝑥𝐹𝑧𝑦𝐹𝑧)))
2221anandis 674 . . . . . . . . . . . 12 ((𝐹 Fn 𝐴 ∧ (𝑥𝐴𝑦𝐴)) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) ↔ (𝑥𝐹𝑧𝑦𝐹𝑧)))
2322pm5.32da 579 . . . . . . . . . . 11 (𝐹 Fn 𝐴 → (((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑥𝐹𝑧𝑦𝐹𝑧))))
2414, 23bitr4d 283 . . . . . . . . . 10 (𝐹 Fn 𝐴 → ((𝑥𝐹𝑧𝑦𝐹𝑧) ↔ ((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)))))
2524imbi1d 343 . . . . . . . . 9 (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ (((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) → 𝑥 = 𝑦)))
26 impexp 451 . . . . . . . . 9 ((((𝑥𝐴𝑦𝐴) ∧ (𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦))) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
2725, 26syl6bb 288 . . . . . . . 8 (𝐹 Fn 𝐴 → (((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))))
2827albidv 1898 . . . . . . 7 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))))
29 19.21v 1917 . . . . . . . 8 (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)))
30 19.23v 1920 . . . . . . . . . 10 (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))
31 fvex 6551 . . . . . . . . . . . 12 (𝐹𝑥) ∈ V
3231eqvinc 3581 . . . . . . . . . . 11 ((𝐹𝑥) = (𝐹𝑦) ↔ ∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)))
3332imbi1i 351 . . . . . . . . . 10 (((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ (∃𝑧(𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦))
3430, 33bitr4i 279 . . . . . . . . 9 (∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦) ↔ ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
3534imbi2i 337 . . . . . . . 8 (((𝑥𝐴𝑦𝐴) → ∀𝑧((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3629, 35bitri 276 . . . . . . 7 (∀𝑧((𝑥𝐴𝑦𝐴) → ((𝑧 = (𝐹𝑥) ∧ 𝑧 = (𝐹𝑦)) → 𝑥 = 𝑦)) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
3728, 36syl6bb 288 . . . . . 6 (𝐹 Fn 𝐴 → (∀𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
38372albidv 1901 . . . . 5 (𝐹 Fn 𝐴 → (∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))))
39 breq1 4965 . . . . . . . 8 (𝑥 = 𝑦 → (𝑥𝐹𝑧𝑦𝐹𝑧))
4039mo4 2607 . . . . . . 7 (∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4140albii 1801 . . . . . 6 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
42 alrot3 2129 . . . . . 6 (∀𝑧𝑥𝑦((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
4341, 42bitri 276 . . . . 5 (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝑦𝑧((𝑥𝐹𝑧𝑦𝐹𝑧) → 𝑥 = 𝑦))
44 r2al 3168 . . . . 5 (∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦) ↔ ∀𝑥𝑦((𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
4538, 43, 443bitr4g 315 . . . 4 (𝐹 Fn 𝐴 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
462, 45syl 17 . . 3 (𝐹:𝐴𝐵 → (∀𝑧∃*𝑥 𝑥𝐹𝑧 ↔ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
4746pm5.32i 575 . 2 ((𝐹:𝐴𝐵 ∧ ∀𝑧∃*𝑥 𝑥𝐹𝑧) ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
481, 47bitri 276 1 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1520   = wceq 1522  wex 1761  wcel 2081  ∃*wmo 2574  wral 3105   class class class wbr 4962  dom cdm 5443   Fn wfn 6220  wf 6221  1-1wf1 6222  cfv 6225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pr 5221
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fv 6233
This theorem is referenced by:  dff13f  6879  f1veqaeq  6880  fpropnf1  6890  dff14a  6893  dff1o6  6897  fcof1  6908  soisoi  6944  f1opr  7069  f1o2ndf1  7671  fnwelem  7678  smo11  7853  tz7.48lem  7928  omsmo  8131  unxpdomlem3  8570  unfilem2  8629  fofinf1o  8645  inf3lem6  8942  r111  9050  fseqenlem1  9296  fodomacn  9328  alephf1  9357  alephiso  9370  ackbij1lem17  9504  infpssrlem5  9575  fin23lem28  9608  fin1a2lem2  9669  fin1a2lem4  9671  axcc2lem  9704  domtriomlem  9710  cnref1o  12234  injresinj  13008  om2uzf1oi  13171  cshf1  14008  wwlktovf1  14155  reeff1  15306  bitsf1  15628  crth  15944  eulerthlem2  15948  1arith  16092  vdwlem12  16157  xpsff1o  16669  setcmon  17176  fthestrcsetc  17229  embedsetcestrclem  17236  fthsetcestrc  17244  yoniso  17364  ghmf1  18128  orbsta  18184  symgextf1  18280  symgfixf1  18296  odf1  18419  kerf1ghm  19187  kerf1hrmOLD  19188  mvrf1  19893  ply1sclf1  20140  znf1o  20380  cygznlem3  20398  uvcf1  20618  lindff1  20646  scmatf1  20824  mdetunilem8  20912  mat2pmatf1  21021  pm2mpf1  21091  ist0-4  22021  ovolicc2lem4  23804  recosf1o  24800  efif1olem4  24810  basellem4  25343  dvdsmulf1o  25453  lgsqrlem2  25605  lgseisenlem2  25634  2lgslem1b  25650  axlowdimlem15  26425  upgrwlkdvdelem  27204  wlkswwlksf1o  27344  wwlksnextinj  27364  clwlkclwwlkf1  27475  clwwlkf1  27515  frgrncvvdeqlem8  27777  numclwwlk1lem2f1  27828  pjmf1  29184  unopf1o  29384  fnpreimac  30106  s3f1  30303  tocyccntz  30423  dff15  31967  f1resrcmplf1d  31974  f1resfz0f1d  31975  erdszelem9  32055  mrsubff1  32370  msubff1  32412  mvhf1  32415  f1omptsnlem  34167  fvineqsnf1  34241  fvineqsneu  34242  poimirlem26  34468  poimirlem27  34469  grpokerinj  34722  cdleme50f1  37229  dihf11  37953  dnnumch3  39151  wessf1ornlem  41004  projf1o  41018  sumnnodd  41472  dvnprodlem1  41792  fourierdlem34  41988  fourierdlem51  42004  fargshiftf1  43103  sprsymrelf1  43160  prproropf1o  43171  fmtnof1  43199  prmdvdsfmtnof1  43251  isomuspgrlem2c  43497  uspgrsprf1  43524  rrx2xpref1o  44206
  Copyright terms: Public domain W3C validator