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

Theorem f1ss 5458
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 5453 . . 3  |-  ( F : A -1-1-> B  ->  F : A --> B )
2 fss 5413 . . 3  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
31, 2sylan 457 . 2  |-  ( ( F : A -1-1-> B  /\  B  C_  C )  ->  F : A --> C )
4 df-f1 5276 . . . 4  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
54simprbi 450 . . 3  |-  ( F : A -1-1-> B  ->  Fun  `' F )
65adantr 451 . 2  |-  ( ( F : A -1-1-> B  /\  B  C_  C )  ->  Fun  `' F
)
7 df-f1 5276 . 2  |-  ( F : A -1-1-> C  <->  ( F : A --> C  /\  Fun  `' F ) )
83, 6, 7sylanbrc 645 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 358    C_ wss 3165   `'ccnv 4704   Fun wfun 5265   -->wf 5267   -1-1->wf1 5268
This theorem is referenced by:  domssex2  7037  1sdom  7081  marypha1lem  7202  marypha2  7208  isinffi  7641  fseqenlem1  7667  dfac12r  7788  ackbij2  7885  cff1  7900  fin23lem28  7982  fin23lem41  7994  pwfseqlem5  8301  hashf1lem1  11409  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumzmhm  15226  gsumzoppg  15232  dvne0f1  19375  erdsze2lem1  23749  eldioph2lem2  26943  eldioph2  26944  lindfres  27396  islindf3  27399  usisuslgra  28247  uslgra1  28252  usgra1  28253
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-f 5275  df-f1 5276
  Copyright terms: Public domain W3C validator