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

Theorem f1ss 6576
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 6571 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 6523 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 580 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 6356 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 497 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 481 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 6356 . 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 3939  ccnv 5552  Fun wfun 6345  wf 6347  1-1wf1 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2803  df-cleq 2817  df-clel 2897  df-in 3946  df-ss 3955  df-f 6355  df-f1 6356
This theorem is referenced by:  f1sng  6652  f1prex  7037  domssex2  8669  1sdom  8713  marypha1lem  8889  marypha2  8895  isinffi  9413  fseqenlem1  9442  dfac12r  9564  ackbij2  9657  cff1  9672  fin23lem28  9754  fin23lem41  9766  pwfseqlem5  10077  hashf1lem1  13806  gsumzres  18951  gsumzcl2  18952  gsumzf1o  18954  gsumzaddlem  18963  gsumzmhm  18979  gsumzoppg  18986  lindfres  20883  islindf3  20886  dvne0f1  24524  istrkg2ld  26160  ausgrusgrb  26865  uspgrushgr  26875  usgruspgr  26878  uspgr1e  26941  sizusglecusglem1  27158  s1f1  30534  s2f1  30536  qqhre  31148  erdsze2lem1  32335  eldioph2lem2  39220  eldioph2  39221
  Copyright terms: Public domain W3C validator