Theorem fss 6724

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 3945	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 33	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 623	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6542	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6542	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 299	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 412	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 400   ⊆ wss 3906  ran crn 5664   Fn wfn 6533  ⟶wf 6534

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ss 3923  df-f 6542

This theorem is referenced by:  fssd  6725  f1ss  6783  fcdmssb  7119  fsn2  7134  fprb  7194  ofco  7701  ffoss  7944  issmo2  8337  smoiso  8350  ssdomg  8998  alephfplem4  10092  cofsmo  10254  fin23lem17  10323  hsmexlem1  10411  axdc3lem4  10438  ac6s  10469  gruen  10798  intgru  10800  ingru  10801  hashf1lem1  14494  sswrd  14561  repsdf2  14817  limsupgre  15534  abscn2  15652  recn2  15654  imcn2  15655  climabs  15657  climre  15659  climim  15660  rlimabs  15662  rlimre  15664  rlimim  15665  caucvgrlem  15726  caurcvgr  15727  caucvgrlem2  15728  caurcvg  15730  fsumre  15862  fsumim  15863  0ram  17081  ramub1  17089  ramcl  17090  acsinfd  18613  acsdomd  18614  gsumval1  18742  resmgmhm2  18771  resmhm2  18881  prdsgrpd  19117  prdsinvgd  19118  symgtrinv  19543  prdscmnd  19932  prdsabld  19933  pgpfaclem1  20154  prdsrngd  20255  prdsmulrcl  20402  prdsringd  20403  prdscrngd  20404  abvf  20899  prdslmodd  21071  zntoslem  21687  regsumsupp  21753  dsmmsubg  21874  dsmmlss  21875  islinds2  21944  lindsmm  21959  lsslindf  21961  psrridm  22093  coe1fval3  22349  1stccnp  23600  1stckgen  23692  prdstps  23767  pthaus  23776  txcmplem2  23780  ptcmpfi  23951  ptcmplem1  24190  ptcmpg  24195  prdstmdd  24262  prdstgpd  24263  ismet2  24471  prdsxmetlem  24506  imasdsf1olem  24511  prdsms  24669  isngp2  24735  metdscn  24995  lmmbr  25398  causs  25438  ovolfioo  25607  ovolficc  25608  ovolfsf  25611  elovolm  25615  ovollb  25619  ovolunlem1a  25636  ovolunlem1  25637  ovolicc2lem1  25657  ovolicc2lem2  25658  ovolicc2lem3  25659  ovolicc2lem4  25660  ovolicc2  25662  uniiccdif  25718  uniioovol  25719  uniiccvol  25720  uniioombllem2  25723  uniioombllem3a  25724  uniioombllem3  25725  uniioombllem4  25726  uniioombllem5  25727  uniioombl  25729  dyadmbl  25740  vitalilem3  25750  vitalilem4  25751  vitalilem5  25752  ismbf  25768  mbfid  25775  0plef  25812  i1f1  25830  i1faddlem  25833  i1fsub  25848  itg1sub  25849  mbfi1fseqlem4  25858  itg2le  25879  itg2mulclem  25886  itg2mulc  25887  itg2monolem1  25890  itg2monolem2  25891  itg2monolem3  25892  itg2mono  25893  itg2i1fseq3  25897  itg2addlem  25898  itg2gt0  25900  itg2cnlem1  25901  itg2cnlem2  25902  dvfre  26091  dvnfre  26092  dvferm1  26125  dvferm2  26127  rolle  26130  dvgt0lem1  26142  dvivthlem1  26148  dvne0  26151  lhop1lem  26153  lhop2  26155  lhop  26156  dvcnvrelem1  26157  dvcnvre  26159  dvcvx  26160  dvfsumrlim  26171  tdeglem3  26197  elplyr  26339  taylthlem2  26515  taylth  26516  ulmcn  26540  iblulm  26548  efcvx  26590  dvrelog  26780  relogcn  26781  dvlog2  26796  leibpi  27085  efrlim  27112  jensenlem2  27130  jensen  27131  amgmlem  27132  amgm  27133  wilthlem2  27211  wilthlem3  27212  basellem7  27229  basellem9  27231  lgsfcl  27447  lgsdchr  27497  dchrvmasumlem1  27637  dchrisum0lem3  27661  axlowdimlem4  29273  axlowdimlem7  29276  axlowdimlem10  29279  upgruhgr  29430  konigsbergssiedgw  30579  pliguhgr  30816  0oo  31119  hhsscms  31608  nlelchi  32391  hmopidmchi  32481  pjinvari  32521  padct  33041  smatrcl  34164  lmlim  34315  rge0scvg  34317  lmdvg  34321  lmdvglim  34322  rrhre  34389  esumfsupre  34439  hashf2  34452  eulerpartlems  34728  eulerpartlemgs2  34748  coinfliprv  34851  fdvposlt  34964  fdvposle  34966  breprexpnat  34999  circlemethnat  35006  circlevma  35007  tgoldbachgtde  35025  lfuhgr  35588  subgrwlk  35602  ptpconn  35703  poimirlem8  38257  poimirlem18  38267  poimirlem21  38270  poimirlem22  38271  mblfinlem2  38287  mbfresfi  38295  itg2addnclem  38300  itg2addnclem2  38301  itg2addnc  38303  itg2gt0cn  38304  ftc1anclem8  38329  fdc  38374  heiborlem6  38445  heibor  38450  lfl0f  39821  intlewftc  42806  sticksstones3  42893  sticksstones9  42899  sticksstones11  42901  sticksstones17  42908  sticksstones18  42909  aks6d1c6lem5  42922  mzpexpmpt  43456  mzpresrename  43461  diophrw  43470  rabren3dioph  43522  lnrfg  43826  seff  44999  sblpnf  45000  binomcxplemnotnn0  45046  stoweidlem44  46738  stirlinglem8  46775  fourierdlem62  46862  fouriersw  46925  nnsum3primes4  48530  grtriclwlk3  48687  zlmodzxzldeplem1  49257  aacllem  50578  amgmwlem  50579