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

Theorem f1ss 5806
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  |-  ( ( F : A -1-1-> B  /\  B  C_  C )  ->  F : A -1-1-> C )

Proof of Theorem f1ss
StepHypRef Expression
1 f1f 5801 . . 3  |-  ( F : A -1-1-> B  ->  F : A --> B )
2 fss 5759 . . 3  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
31, 2sylan 478 . 2  |-  ( ( F : A -1-1-> B  /\  B  C_  C )  ->  F : A --> C )
4 df-f1 5605 . . . 4  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
54simprbi 470 . . 3  |-  ( F : A -1-1-> B  ->  Fun  `' F )
65adantr 471 . 2  |-  ( ( F : A -1-1-> B  /\  B  C_  C )  ->  Fun  `' F
)
7 df-f1 5605 . 2  |-  ( F : A -1-1-> C  <->  ( F : A --> C  /\  Fun  `' F ) )
83, 6, 7sylanbrc 675 1  |-  ( ( F : A -1-1-> B  /\  B  C_  C )  ->  F : A -1-1-> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    C_ wss 3415   `'ccnv 4851   Fun wfun 5594   -->wf 5596   -1-1->wf1 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-in 3422  df-ss 3429  df-f 5604  df-f1 5605
This theorem is referenced by:  f1prex  6206  domssex2  7757  1sdom  7800  marypha1lem  7972  marypha2  7978  isinffi  8451  fseqenlem1  8480  dfac12r  8601  ackbij2  8698  cff1  8713  fin23lem28  8795  fin23lem41  8807  pwfseqlem5  9113  hashf1lem1  12650  gsumzres  17591  gsumzcl2  17592  gsumzf1o  17594  gsumzaddlem  17602  gsumzmhm  17618  gsumzoppg  17625  lindfres  19429  islindf3  19432  dvne0f1  23012  istrkg2ld  24556  ausisusgra  25130  uslisushgra  25138  usisuslgra  25140  uslgra1  25147  usgra1  25148  sizeusglecusglem1  25260  2trllemE  25331  constr1trl  25366  frgrancvvdeqlem8  25816  qqhre  28872  erdsze2lem1  29974  eldioph2lem2  35647  eldioph2  35648  ausgrusgrb  39299  uspgrushgr  39309  usgruspgr  39312  uspgr1e  39368  sizusglecusglem1  39571
  Copyright terms: Public domain W3C validator