Theorem fss 6729

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3908  ran crn 5667   Fn wfn 6538  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3925  df-f 6547

This theorem is used by:  fssd  6730  f1ss  6788  fcdmssb  7124  fsn2  7139  fprb  7199  ofco  7712  ffoss  7952  issmo2  8345  smoiso  8358  ssdomg  9006  alephfplem4  10110  cofsmo  10271  fin23lem17  10340  hsmexlem1  10428  axdc3lem4  10455  ac6s  10486  gruen  10815  intgru  10817  ingru  10818  hashf1lem1  14512  sswrd  14579  repsdf2  14841  limsupgre  15558  abscn2  15676  recn2  15678  imcn2  15679  climabs  15681  climre  15683  climim  15684  rlimabs  15686  rlimre  15688  rlimim  15689  caucvgrlem  15750  caurcvgr  15751  caucvgrlem2  15752  caurcvg  15754  fsumre  15886  fsumim  15887  0ram  17105  ramub1  17113  ramcl  17114  acsinfd  18637  acsdomd  18638  gsumval1  18766  resmgmhm2  18795  resmhm2  18905  prdsgrpd  19141  prdsinvgd  19142  symgtrinv  19567  prdscmnd  19956  prdsabld  19957  pgpfaclem1  20178  prdsrngd  20279  prdsmulrcl  20427  prdsringd  20428  prdscrngd  20429  abvf  20948  prdslmodd  21120  zntoslem  21736  regsumsupp  21802  dsmmsubg  21923  dsmmlss  21924  islinds2  21993  lindsmm  22008  lsslindf  22010  psrridm  22142  coe1fval3  22398  1stccnp  23649  1stckgen  23741  prdstps  23816  pthaus  23825  txcmplem2  23829  ptcmpfi  24000  ptcmplem1  24239  ptcmpg  24244  prdstmdd  24311  prdstgpd  24312  ismet2  24520  prdsxmetlem  24555  imasdsf1olem  24560  prdsms  24718  isngp2  24784  metdscn  25044  lmmbr  25447  causs  25487  ovolfioo  25656  ovolficc  25657  ovolfsf  25660  elovolm  25664  ovollb  25668  ovolunlem1a  25685  ovolunlem1  25686  ovolicc2lem1  25706  ovolicc2lem2  25707  ovolicc2lem3  25708  ovolicc2lem4  25709  ovolicc2  25711  uniiccdif  25767  uniioovol  25768  uniiccvol  25769  uniioombllem2  25772  uniioombllem3a  25773  uniioombllem3  25774  uniioombllem4  25775  uniioombllem5  25776  uniioombl  25778  dyadmbl  25789  vitalilem3  25799  vitalilem4  25800  vitalilem5  25801  ismbf  25817  mbfid  25824  0plef  25861  i1f1  25879  i1faddlem  25882  i1fsub  25897  itg1sub  25898  mbfi1fseqlem4  25907  itg2le  25928  itg2mulclem  25935  itg2mulc  25936  itg2monolem1  25939  itg2monolem2  25940  itg2monolem3  25941  itg2mono  25942  itg2i1fseq3  25946  itg2addlem  25947  itg2gt0  25949  itg2cnlem1  25950  itg2cnlem2  25951  dvfre  26140  dvnfre  26141  dvferm1  26174  dvferm2  26176  rolle  26179  dvgt0lem1  26191  dvivthlem1  26197  dvne0  26200  lhop1lem  26202  lhop2  26204  lhop  26205  dvcnvrelem1  26206  dvcnvre  26208  dvcvx  26209  dvfsumrlim  26220  tdeglem3  26246  elplyr  26388  taylthlem2  26567  taylth  26568  ulmcn  26592  iblulm  26600  efcvx  26642  dvrelog  26832  relogcn  26833  dvlog2  26848  leibpi  27137  efrlim  27164  jensenlem2  27182  jensen  27183  amgmlem  27184  amgm  27185  wilthlem2  27263  wilthlem3  27264  basellem7  27281  basellem9  27283  lgsfcl  27499  lgsdchr  27549  dchrvmasumlem1  27689  dchrisum0lem3  27713  axlowdimlem4  29325  axlowdimlem7  29328  axlowdimlem10  29331  upgruhgr  29482  konigsbergssiedgw  30631  pliguhgr  30868  0oo  31171  hhsscms  31660  nlelchi  32443  hmopidmchi  32533  pjinvari  32573  padct  33093  smatrcl  34210  lmlim  34361  rge0scvg  34363  lmdvg  34367  lmdvglim  34368  rrhre  34435  esumfsupre  34485  hashf2  34498  eulerpartlems  34774  eulerpartlemgs2  34794  coinfliprv  34897  fdvposlt  35010  fdvposle  35012  breprexpnat  35045  circlemethnat  35052  circlevma  35053  tgoldbachgtde  35071  lfuhgr  35623  subgrwlk  35637  ptpconn  35738  poimirlem8  38312  poimirlem18  38322  poimirlem21  38325  poimirlem22  38326  mblfinlem2  38342  mbfresfi  38350  itg2addnclem  38355  itg2addnclem2  38356  itg2addnc  38358  itg2gt0cn  38359  ftc1anclem8  38384  fdc  38429  heiborlem6  38500  heibor  38505  lfl0f  39876  intlewftc  42861  sticksstones3  42948  sticksstones9  42954  sticksstones11  42956  sticksstones17  42963  sticksstones18  42964  aks6d1c6lem5  42977  mzpexpmpt  43509  mzpresrename  43514  diophrw  43523  rabren3dioph  43575  lnrfg  43879  seff  45052  sblpnf  45053  binomcxplemnotnn0  45099  stoweidlem44  46791  stirlinglem8  46828  fourierdlem62  46915  fouriersw  46978  nnsum3primes4  48586  grtriclwlk3  48743  zlmodzxzldeplem1  49313  aacllem  50654  amgmwlem  50683