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

Step	Hyp	Ref	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 )
3	1, 2	sylan 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 ) )
5	4	simprbi 470	. . 3 |- ( F : A -1-1-> B -> Fun `' F )
6	5	adantr 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 ) )
8	3, 6, 7	sylanbrc 675	1 |- ( ( F : A -1-1-> B /\ B C_ C ) -> F : A -1-1-> C )

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