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

Theorem f1ores 6049
Description: The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by NM, 25-Mar-1998.)
Assertion
Ref Expression
f1ores ((𝐹:𝐴1-1𝐵𝐶𝐴) → (𝐹𝐶):𝐶1-1-onto→(𝐹𝐶))

Proof of Theorem f1ores
StepHypRef Expression
1 f1ssres 6006 . . 3 ((𝐹:𝐴1-1𝐵𝐶𝐴) → (𝐹𝐶):𝐶1-1𝐵)
2 f1f1orn 6046 . . 3 ((𝐹𝐶):𝐶1-1𝐵 → (𝐹𝐶):𝐶1-1-onto→ran (𝐹𝐶))
31, 2syl 17 . 2 ((𝐹:𝐴1-1𝐵𝐶𝐴) → (𝐹𝐶):𝐶1-1-onto→ran (𝐹𝐶))
4 df-ima 5041 . . 3 (𝐹𝐶) = ran (𝐹𝐶)
5 f1oeq3 6027 . . 3 ((𝐹𝐶) = ran (𝐹𝐶) → ((𝐹𝐶):𝐶1-1-onto→(𝐹𝐶) ↔ (𝐹𝐶):𝐶1-1-onto→ran (𝐹𝐶)))
64, 5ax-mp 5 . 2 ((𝐹𝐶):𝐶1-1-onto→(𝐹𝐶) ↔ (𝐹𝐶):𝐶1-1-onto→ran (𝐹𝐶))
73, 6sylibr 223 1 ((𝐹:𝐴1-1𝐵𝐶𝐴) → (𝐹𝐶):𝐶1-1-onto→(𝐹𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383   = wceq 1475  wss 3540  ran crn 5029  cres 5030  cima 5031  1-1wf1 5787  1-1-ontowf1o 5789
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4579  df-opab 4639  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797
This theorem is referenced by:  f1imacnv  6051  f1oresrab  6287  isores3  6463  isoini2  6467  f1imaeng  7880  f1imaen2g  7881  domunsncan  7923  php3  8009  ssfi  8043  infdifsn  8415  infxpenlem  8697  ackbij2lem2  8923  fin1a2lem6  9088  grothomex  9508  fsumss  14252  ackbijnn  14348  fprodss  14466  unbenlem  15399  eqgen  17419  symgfixelsi  17627  gsumval3lem1  18078  gsumval3lem2  18079  gsumzaddlem  18093  coe1mul2lem2  19408  lindsmm  19934  tsmsf1o  21706  ovoliunlem1  23022  dvcnvrelem2  23530  logf1o2  24141  dvlog  24142  eupares  26296  adjbd1o  28122  rinvf1o  28608  padct  28679  indf1ofs  29209  eulerpartgbij  29555  eulerpartlemgh  29561  ballotlemfrc  29709  erdsze2lem2  30234  poimirlem4  32377  poimirlem9  32382  ismtyres  32571  pwfi2f1o  36478  sge0f1o  39069  ushgredgedga  40448  ushgredgedgaloop  40450  trlreslem  40899
  Copyright terms: Public domain W3C validator