Theorem f1ss 5711

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 5706	. . 3 |- ( F : A -1-1-> B -> F : A --> B )
2		fss 5667	. . 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 5523	. . . 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 5523	. 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 3428   `'ccnv 4939   Fun wfun 5512   -->wf 5514   -1-1->wf1 5515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3435  df-ss 3442  df-f 5522  df-f1 5523

This theorem is referenced by:  domssex2  7573  1sdom  7618  marypha1lem  7786  marypha2  7792  isinffi  8265  fseqenlem1  8297  dfac12r  8418  ackbij2  8515  cff1  8530  fin23lem28  8612  fin23lem41  8624  pwfseqlem5  8933  hashf1lem1  12312  gsumzres  16494  gsumzcl2  16495  gsumzf1o  16497  gsumzresOLD  16498  gsumzclOLD  16499  gsumzf1oOLD  16500  gsumzaddlem  16514  gsumzaddlemOLD  16516  gsumzmhm  16537  gsumzmhmOLD  16538  gsumzoppg  16547  gsumzoppgOLD  16548  lindfres  18363  islindf3  18366  dvne0f1  21602  istrkg2ld  23040  ausisusgra  23416  usisuslgra  23423  uslgra1  23428  usgra1  23429  sizeusglecusglem1  23529  2trllemE  23589  constr1trl  23624  qqhre  26582  erdsze2lem1  27227  eldioph2lem2  29239  eldioph2  29240  frgrancvvdeqlem8  30773