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

Theorem f1ss 5646
Description: A function that is one-to-one is also one-to-one on some superset of its range. (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 5641 . . 3  |-  ( F : A -1-1-> B  ->  F : A --> B )
2 fss 5601 . . 3  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
31, 2sylan 459 . 2  |-  ( ( F : A -1-1-> B  /\  B  C_  C )  ->  F : A --> C )
4 df-f1 5461 . . . 4  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
54simprbi 452 . . 3  |-  ( F : A -1-1-> B  ->  Fun  `' F )
65adantr 453 . 2  |-  ( ( F : A -1-1-> B  /\  B  C_  C )  ->  Fun  `' F
)
7 df-f1 5461 . 2  |-  ( F : A -1-1-> C  <->  ( F : A --> C  /\  Fun  `' F ) )
83, 6, 7sylanbrc 647 1  |-  ( ( F : A -1-1-> B  /\  B  C_  C )  ->  F : A -1-1-> C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    C_ wss 3322   `'ccnv 4879   Fun wfun 5450   -->wf 5452   -1-1->wf1 5453
This theorem is referenced by:  domssex2  7269  1sdom  7313  marypha1lem  7440  marypha2  7446  isinffi  7881  fseqenlem1  7907  dfac12r  8028  ackbij2  8125  cff1  8140  fin23lem28  8222  fin23lem41  8234  pwfseqlem5  8540  hashf1lem1  11706  gsumzres  15519  gsumzcl  15520  gsumzf1o  15521  gsumzaddlem  15528  gsumzmhm  15535  gsumzoppg  15541  dvne0f1  19898  ausisusgra  21382  usisuslgra  21389  uslgra1  21394  usgra1  21395  sizeusglecusglem1  21495  2trllemE  21555  constr1trl  21590  qqhre  24388  erdsze2lem1  24891  eldioph2lem2  26821  eldioph2  26822  lindfres  27272  islindf3  27275  frgrancvvdeqlem8  28431
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336  df-f 5460  df-f1 5461
  Copyright terms: Public domain W3C validator