Theorem fss 6722

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 3965	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 612	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6535	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6535	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 296	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 407	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3926  ran crn 5655   Fn wfn 6526  ⟶wf 6527

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3943  df-f 6535

This theorem is referenced by:  fssd  6723  f1ss  6779  fcdmssb  7112  fsn2  7126  fprb  7186  ofco  7696  ffoss  7944  issmo2  8363  smoiso  8376  ssdomg  9014  alephfplem4  10121  cofsmo  10283  fin23lem17  10352  hsmexlem1  10440  axdc3lem4  10467  ac6s  10498  gruen  10826  intgru  10828  ingru  10829  hashf1lem1  14473  sswrd  14540  repsdf2  14796  limsupgre  15497  abscn2  15615  recn2  15617  imcn2  15618  climabs  15620  climre  15622  climim  15623  rlimabs  15625  rlimre  15627  rlimim  15628  caucvgrlem  15689  caurcvgr  15690  caucvgrlem2  15691  caurcvg  15693  fsumre  15824  fsumim  15825  0ram  17040  ramub1  17048  ramcl  17049  acsinfd  18566  acsdomd  18567  gsumval1  18661  resmgmhm2  18690  resmhm2  18799  prdsgrpd  19033  prdsinvgd  19034  symgtrinv  19453  prdscmnd  19842  prdsabld  19843  pgpfaclem1  20064  prdsrngd  20136  prdsmulrcl  20280  prdsringd  20281  prdscrngd  20282  abvf  20775  prdslmodd  20926  zntoslem  21517  regsumsupp  21582  dsmmsubg  21703  dsmmlss  21704  islinds2  21773  lindsmm  21788  lsslindf  21790  psrridm  21923  coe1fval3  22144  1stccnp  23400  1stckgen  23492  prdstps  23567  pthaus  23576  txcmplem2  23580  ptcmpfi  23751  ptcmplem1  23990  ptcmpg  23995  prdstmdd  24062  prdstgpd  24063  ismet2  24272  prdsxmetlem  24307  imasdsf1olem  24312  prdsms  24470  isngp2  24536  metdscn  24796  lmmbr  25210  causs  25250  ovolfioo  25420  ovolficc  25421  ovolfsf  25424  elovolm  25428  ovollb  25432  ovolunlem1a  25449  ovolunlem1  25450  ovolicc2lem1  25470  ovolicc2lem2  25471  ovolicc2lem3  25472  ovolicc2lem4  25473  ovolicc2  25475  uniiccdif  25531  uniioovol  25532  uniiccvol  25533  uniioombllem2  25536  uniioombllem3a  25537  uniioombllem3  25538  uniioombllem4  25539  uniioombllem5  25540  uniioombl  25542  dyadmbl  25553  vitalilem3  25563  vitalilem4  25564  vitalilem5  25565  ismbf  25581  mbfid  25588  0plef  25625  i1f1  25643  i1faddlem  25646  i1fsub  25661  itg1sub  25662  mbfi1fseqlem4  25671  itg2le  25692  itg2mulclem  25699  itg2mulc  25700  itg2monolem1  25703  itg2monolem2  25704  itg2monolem3  25705  itg2mono  25706  itg2i1fseq3  25710  itg2addlem  25711  itg2gt0  25713  itg2cnlem1  25714  itg2cnlem2  25715  dvfre  25907  dvnfre  25908  dvferm1  25941  dvferm2  25943  rolle  25946  dvgt0lem1  25959  dvivthlem1  25965  dvne0  25968  lhop1lem  25970  lhop2  25972  lhop  25973  dvcnvrelem1  25974  dvcnvre  25976  dvcvx  25977  dvfsumrlim  25990  tdeglem3  26016  elplyr  26158  taylthlem2  26334  taylthlem2OLD  26335  taylth  26336  ulmcn  26360  iblulm  26368  efcvx  26411  dvrelog  26598  relogcn  26599  dvlog2  26614  leibpi  26904  efrlim  26931  efrlimOLD  26932  jensenlem2  26950  jensen  26951  amgmlem  26952  amgm  26953  wilthlem2  27031  wilthlem3  27032  basellem7  27049  basellem9  27051  lgsfcl  27268  lgsdchr  27318  dchrvmasumlem1  27458  dchrisum0lem3  27482  axlowdimlem4  28924  axlowdimlem7  28927  axlowdimlem10  28930  upgruhgr  29081  konigsbergssiedgw  30231  pliguhgr  30467  0oo  30770  hhsscms  31259  nlelchi  32042  hmopidmchi  32132  pjinvari  32172  padct  32697  smatrcl  33827  lmlim  33978  rge0scvg  33980  lmdvg  33984  lmdvglim  33985  rrhre  34052  esumfsupre  34102  hashf2  34115  eulerpartlems  34392  eulerpartlemgs2  34412  coinfliprv  34515  fdvposlt  34631  fdvposle  34633  breprexpnat  34666  circlemethnat  34673  circlevma  34674  tgoldbachgtde  34692  lfuhgr  35140  subgrwlk  35154  ptpconn  35255  poimirlem8  37652  poimirlem18  37662  poimirlem21  37665  poimirlem22  37666  mblfinlem2  37682  mbfresfi  37690  itg2addnclem  37695  itg2addnclem2  37696  itg2addnc  37698  itg2gt0cn  37699  ftc1anclem8  37724  fdc  37769  heiborlem6  37840  heibor  37845  lfl0f  39087  intlewftc  42074  sticksstones3  42161  sticksstones9  42167  sticksstones11  42169  sticksstones17  42176  sticksstones18  42177  aks6d1c6lem5  42190  mzpexpmpt  42768  mzpresrename  42773  diophrw  42782  rabren3dioph  42838  lnrfg  43143  seff  44333  sblpnf  44334  binomcxplemnotnn0  44380  stoweidlem44  46073  stirlinglem8  46110  fourierdlem62  46197  fouriersw  46260  nnsum3primes4  47802  grtriclwlk3  47957  zlmodzxzldeplem1  48476  aacllem  49665  amgmwlem  49666