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

Theorem f1ss 6247
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 6242 . . 3 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
2 fss 6197 . . 3 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
31, 2sylan 563 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
4 df-f1 6037 . . . 4 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ Fun 𝐹))
54simprbi 480 . . 3 (𝐹:𝐴1-1𝐵 → Fun 𝐹)
65adantr 466 . 2 ((𝐹:𝐴1-1𝐵𝐵𝐶) → Fun 𝐹)
7 df-f1 6037 . 2 (𝐹:𝐴1-1𝐶 ↔ (𝐹:𝐴𝐶 ∧ Fun 𝐹))
83, 6, 7sylanbrc 566 1 ((𝐹:𝐴1-1𝐵𝐵𝐶) → 𝐹:𝐴1-1𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wss 3724  ccnv 5249  Fun wfun 6026  wf 6028  1-1wf1 6029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3731  df-ss 3738  df-f 6036  df-f1 6037
This theorem is referenced by:  f1sng  6320  f1prex  6683  domssex2  8277  1sdom  8320  marypha1lem  8496  marypha2  8502  isinffi  9019  fseqenlem1  9048  dfac12r  9171  ackbij2  9268  cff1  9283  fin23lem28  9365  fin23lem41  9377  pwfseqlem5  9688  hashf1lem1  13442  gsumzres  18518  gsumzcl2  18519  gsumzf1o  18521  gsumzaddlem  18529  gsumzmhm  18545  gsumzoppg  18552  lindfres  20380  islindf3  20383  dvne0f1  23996  istrkg2ld  25581  ausgrusgrb  26283  uspgrushgr  26293  usgruspgr  26296  uspgr1e  26360  sizusglecusglem1  26593  qqhre  30405  erdsze2lem1  31524  eldioph2lem2  37851  eldioph2  37852
  Copyright terms: Public domain W3C validator