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

Theorem f1ss 6573
Description: A function that is one-to-one is also one-to-one on some superset of its codomain. (Contributed by Mario Carneiro, 12-Jan-2013.)
Assertion
Ref Expression
f1ss ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)

Proof of Theorem f1ss
StepHypRef Expression
1 f1f 6568 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 6520 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 580 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 6353 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 497 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 481 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 6353 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 583 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wss 3933  ccnv 5547  Fun wfun 6342  wf 6344  1-1wf1 6345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-in 3940  df-ss 3949  df-f 6352  df-f1 6353
This theorem is referenced by:  f1sng  6649  f1prex  7031  domssex2  8665  1sdom  8709  marypha1lem  8885  marypha2  8891  isinffi  9409  fseqenlem1  9438  dfac12r  9560  ackbij2  9653  cff1  9668  fin23lem28  9750  fin23lem41  9762  pwfseqlem5  10073  hashf1lem1  13801  gsumzres  18958  gsumzcl2  18959  gsumzf1o  18961  gsumzaddlem  18970  gsumzmhm  18986  gsumzoppg  18993  lindfres  20895  islindf3  20898  dvne0f1  24536  istrkg2ld  26173  ausgrusgrb  26877  uspgrushgr  26887  usgruspgr  26890  uspgr1e  26953  sizusglecusglem1  27170  s1f1  30546  s2f1  30548  qqhre  31160  erdsze2lem1  32347  eldioph2lem2  39236  eldioph2  39237  fundcmpsurbijinjpreimafv  43444  fundcmpsurinjimaid  43448
  Copyright terms: Public domain W3C validator