Theorem f1ss 5772

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 5767	. . 3 |- ( F : A -1-1-> B -> F : A --> B )
2		fss 5725	. . 3 |- ( ( F : A --> B /\ B C_ C ) -> F : A --> C )
3	1, 2	sylan 471	. 2 |- ( ( F : A -1-1-> B /\ B C_ C ) -> F : A --> C )
4		df-f1 5579	. . . 4 |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
5	4	simprbi 464	. . 3 |- ( F : A -1-1-> B -> Fun `' F )
6	5	adantr 465	. 2 |- ( ( F : A -1-1-> B /\ B C_ C ) -> Fun `' F )
7		df-f1 5579	. 2 |- ( F : A -1-1-> C <-> ( F : A --> C /\ Fun `' F ) )
8	3, 6, 7	sylanbrc 664	1 |- ( ( F : A -1-1-> B /\ B C_ C ) -> F : A -1-1-> C )

Syntax hints:   -> wi 4   /\ wa 369   C_ wss 3458   `'ccnv 4984   Fun wfun 5568   -->wf 5570   -1-1->wf1 5571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472  df-f 5578  df-f1 5579

This theorem is referenced by:  domssex2  7675  1sdom  7720  marypha1lem  7891  marypha2  7897  isinffi  8371  fseqenlem1  8403  dfac12r  8524  ackbij2  8621  cff1  8636  fin23lem28  8718  fin23lem41  8730  pwfseqlem5  9039  hashf1lem1  12478  gsumzres  16783  gsumzcl2  16784  gsumzf1o  16786  gsumzresOLD  16787  gsumzclOLD  16788  gsumzf1oOLD  16789  gsumzaddlem  16803  gsumzaddlemOLD  16805  gsumzmhm  16826  gsumzmhmOLD  16827  gsumzoppg  16836  gsumzoppgOLD  16837  lindfres  18725  islindf3  18728  dvne0f1  22279  istrkg2ld  23723  ausisusgra  24220  uslisushgra  24228  usisuslgra  24230  uslgra1  24237  usgra1  24238  sizeusglecusglem1  24349  2trllemE  24420  constr1trl  24455  frgrancvvdeqlem8  24905  qqhre  27864  erdsze2lem1  28513  eldioph2lem2  30662  eldioph2  30663