Theorem fss 6678

Description: Expanding the codomain of a mapping. (Contributed by NM, 10-May-1998.) (Proof shortened by Andrew Salmon, 17-Sep-2011.)

Assertion

Ref	Expression
fss	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Proof of Theorem fss

Step	Hyp	Ref	Expression
1		sstr2 3929	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 618	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6496	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6496	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 297	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 408	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3890  ran crn 5626   Fn wfn 6487  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816

This theorem depends on definitions:  df-bi 208  df-an 397  df-ss 3907  df-f 6496

This theorem is referenced by:  fssd  6679  f1ss  6735  fcdmssb  7070  fsn2  7085  fprb  7145  ofco  7652  ffoss  7895  issmo2  8286  smoiso  8299  ssdomg  8944  alephfplem4  10027  cofsmo  10189  fin23lem17  10258  hsmexlem1  10346  axdc3lem4  10373  ac6s  10404  gruen  10733  intgru  10735  ingru  10736  hashf1lem1  14415  sswrd  14482  repsdf2  14738  limsupgre  15441  abscn2  15559  recn2  15561  imcn2  15562  climabs  15564  climre  15566  climim  15567  rlimabs  15569  rlimre  15571  rlimim  15572  caucvgrlem  15633  caurcvgr  15634  caucvgrlem2  15635  caurcvg  15637  fsumre  15769  fsumim  15770  0ram  16989  ramub1  16997  ramcl  16998  acsinfd  18520  acsdomd  18521  gsumval1  18649  resmgmhm2  18678  resmhm2  18787  prdsgrpd  19024  prdsinvgd  19025  symgtrinv  19445  prdscmnd  19834  prdsabld  19835  pgpfaclem1  20056  prdsrngd  20155  prdsmulrcl  20297  prdsringd  20298  prdscrngd  20299  abvf  20794  prdslmodd  20966  zntoslem  21538  regsumsupp  21604  dsmmsubg  21725  dsmmlss  21726  islinds2  21795  lindsmm  21810  lsslindf  21812  psrridm  21944  coe1fval3  22200  1stccnp  23452  1stckgen  23544  prdstps  23619  pthaus  23628  txcmplem2  23632  ptcmpfi  23803  ptcmplem1  24042  ptcmpg  24047  prdstmdd  24114  prdstgpd  24115  ismet2  24323  prdsxmetlem  24358  imasdsf1olem  24363  prdsms  24521  isngp2  24587  metdscn  24847  lmmbr  25250  causs  25290  ovolfioo  25459  ovolficc  25460  ovolfsf  25463  elovolm  25467  ovollb  25471  ovolunlem1a  25488  ovolunlem1  25489  ovolicc2lem1  25509  ovolicc2lem2  25510  ovolicc2lem3  25511  ovolicc2lem4  25512  ovolicc2  25514  uniiccdif  25570  uniioovol  25571  uniiccvol  25572  uniioombllem2  25575  uniioombllem3a  25576  uniioombllem3  25577  uniioombllem4  25578  uniioombllem5  25579  uniioombl  25581  dyadmbl  25592  vitalilem3  25602  vitalilem4  25603  vitalilem5  25604  ismbf  25620  mbfid  25627  0plef  25664  i1f1  25682  i1faddlem  25685  i1fsub  25700  itg1sub  25701  mbfi1fseqlem4  25710  itg2le  25731  itg2mulclem  25738  itg2mulc  25739  itg2monolem1  25742  itg2monolem2  25743  itg2monolem3  25744  itg2mono  25745  itg2i1fseq3  25749  itg2addlem  25750  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  dvfre  25943  dvnfre  25944  dvferm1  25977  dvferm2  25979  rolle  25982  dvgt0lem1  25994  dvivthlem1  26000  dvne0  26003  lhop1lem  26005  lhop2  26007  lhop  26008  dvcnvrelem1  26009  dvcnvre  26011  dvcvx  26012  dvfsumrlim  26023  tdeglem3  26049  elplyr  26191  taylthlem2  26364  taylth  26365  ulmcn  26389  iblulm  26397  efcvx  26439  dvrelog  26626  relogcn  26627  dvlog2  26642  leibpi  26931  efrlim  26958  jensenlem2  26976  jensen  26977  amgmlem  26978  amgm  26979  wilthlem2  27057  wilthlem3  27058  basellem7  27075  basellem9  27077  lgsfcl  27293  lgsdchr  27343  dchrvmasumlem1  27483  dchrisum0lem3  27507  axlowdimlem4  29039  axlowdimlem7  29042  axlowdimlem10  29045  upgruhgr  29196  konigsbergssiedgw  30345  pliguhgr  30582  0oo  30885  hhsscms  31374  nlelchi  32157  hmopidmchi  32247  pjinvari  32287  padct  32817  smatrcl  33987  lmlim  34138  rge0scvg  34140  lmdvg  34144  lmdvglim  34145  rrhre  34212  esumfsupre  34262  hashf2  34275  eulerpartlems  34551  eulerpartlemgs2  34571  coinfliprv  34674  fdvposlt  34790  fdvposle  34792  breprexpnat  34825  circlemethnat  34832  circlevma  34833  tgoldbachgtde  34851  lfuhgr  35353  subgrwlk  35367  ptpconn  35468  poimirlem8  38002  poimirlem18  38012  poimirlem21  38015  poimirlem22  38016  mblfinlem2  38032  mbfresfi  38040  itg2addnclem  38045  itg2addnclem2  38046  itg2addnc  38048  itg2gt0cn  38049  ftc1anclem8  38074  fdc  38119  heiborlem6  38190  heibor  38195  lfl0f  39568  intlewftc  42553  sticksstones3  42640  sticksstones9  42646  sticksstones11  42648  sticksstones17  42655  sticksstones18  42656  aks6d1c6lem5  42669  mzpexpmpt  43201  mzpresrename  43206  diophrw  43215  rabren3dioph  43267  lnrfg  43571  seff  44760  sblpnf  44761  binomcxplemnotnn0  44807  stoweidlem44  46494  stirlinglem8  46531  fourierdlem62  46618  fouriersw  46681  nnsum3primes4  48286  grtriclwlk3  48443  zlmodzxzldeplem1  48998  aacllem  50298  amgmwlem  50299