Theorem fss 6748

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 3920	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 33	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 624	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6562	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6562	. . 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 3900  ran crn 5656   Fn wfn 6553  ⟶wf 6554

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 3901  df-f 6562

This theorem is used by:  fssd  6749  f1ss  6807  fcdmssb  7146  fsn2  7161  fprb  7222  ofco  7742  ffoss  7982  issmo2  8385  smoiso  8398  ssdomg  9055  alephfplem4  10213  cofsmo  10374  fin23lem17  10443  hsmexlem1  10531  axdc3lem4  10558  ac6s  10589  gruen  10924  intgru  10926  ingru  10927  hashf1lem1  14627  sswrd  14694  repsdf2  14957  limsupgre  15677  abscn2  15795  recn2  15797  imcn2  15798  climabs  15800  climre  15802  climim  15803  rlimabs  15805  rlimre  15807  rlimim  15808  caucvgrlem  15869  caurcvgr  15870  caucvgrlem2  15871  caurcvg  15873  fsumre  16004  fsumim  16005  0ram  17227  ramub1  17235  ramcl  17236  acsinfd  18759  acsdomd  18760  gsumval1  18901  resmgmhm2  18930  resmhm2  19046  prdsgrpd  19289  prdsinvgd  19290  symgtrinv  19716  prdscmnd  20105  prdsabld  20106  pgpfaclem1  20327  prdsrngd  20428  prdsmulrcl  20579  prdsringd  20580  prdscrngd  20581  abvf  21102  prdslmodd  21274  zntoslem  21892  regsumsupp  21958  dsmmsubg  22079  dsmmlss  22080  islinds2  22149  lindsmm  22164  lsslindf  22166  psrridm  22300  coe1fval3  22556  1stccnp  23811  1stckgen  23903  prdstps  23978  pthaus  23987  txcmplem2  23991  ptcmpfi  24162  ptcmplem1  24401  ptcmpg  24406  prdstmdd  24473  prdstgpd  24474  ismet2  24682  prdsxmetlem  24717  imasdsf1olem  24722  prdsms  24880  isngp2  24946  metdscn  25206  lmmbr  25609  causs  25649  ovolfioo  25818  ovolficc  25819  ovolfsf  25822  elovolm  25826  ovollb  25830  ovolunlem1a  25847  ovolunlem1  25848  ovolicc2lem1  25868  ovolicc2lem2  25869  ovolicc2lem3  25870  ovolicc2lem4  25871  ovolicc2  25873  uniiccdif  25929  uniioovol  25930  uniiccvol  25931  uniioombllem2  25934  uniioombllem3a  25935  uniioombllem3  25936  uniioombllem4  25937  uniioombllem5  25938  uniioombl  25940  dyadmbl  25951  vitalilem3  25961  vitalilem4  25962  vitalilem5  25963  ismbf  25979  mbfid  25986  0plef  26023  i1f1  26041  i1faddlem  26044  i1fsub  26059  itg1sub  26060  mbfi1fseqlem4  26069  itg2le  26090  itg2mulclem  26097  itg2mulc  26098  itg2monolem1  26101  itg2monolem2  26102  itg2monolem3  26103  itg2mono  26104  itg2i1fseq3  26108  itg2addlem  26109  itg2gt0  26111  itg2cnlem1  26112  itg2cnlem2  26113  dvfre  26301  dvnfre  26302  dvferm1  26335  dvferm2  26337  rolle  26340  dvgt0lem1  26352  dvivthlem1  26358  dvne0  26361  lhop1lem  26363  lhop2  26365  lhop  26366  dvcnvrelem1  26367  dvcnvre  26369  dvcvx  26370  dvfsumrlim  26381  tdeglem3  26407  elplyr  26549  taylthlem2  26731  taylth  26732  ulmcn  26756  iblulm  26764  efcvx  26806  dvrelog  26995  relogcn  26996  dvlog2  27011  leibpi  27300  efrlim  27327  jensenlem2  27345  jensen  27346  amgmlem  27347  amgm  27348  wilthlem2  27426  wilthlem3  27427  basellem7  27444  basellem9  27446  lgsfcl  27662  lgsdchr  27712  dchrvmasumlem1  27852  dchrisum0lem3  27876  axlowdimlem4  29553  axlowdimlem7  29556  axlowdimlem10  29559  upgruhgr  29710  lfuhgr  29756  subgrwlk  30299  konigsbergssiedgw  30881  pliguhgr  31118  0oo  31421  hhsscms  31910  nlelchi  32693  hmopidmchi  32783  pjinvari  32823  padct  33381  smatrcl  34498  lmlim  34649  rge0scvg  34651  lmdvg  34655  lmdvglim  34656  rrhre  34723  esumfsupre  34773  hashf2  34786  eulerpartlems  35062  eulerpartlemgs2  35082  coinfliprv  35185  fdvposlt  35298  fdvposle  35300  breprexpnat  35333  circlemethnat  35340  circlevma  35341  tgoldbachgtde  35359  ptpconn  36165  poimirlem8  38738  poimirlem18  38748  poimirlem21  38751  poimirlem22  38752  mblfinlem2  38768  mbfresfi  38776  itg2addnclem  38781  itg2addnclem2  38782  itg2addnc  38784  itg2gt0cn  38785  ftc1anclem8  38810  fdc  38871  heiborlem6  38942  heibor  38947  lfl0f  40318  intlewftc  43303  sticksstones3  43390  sticksstones9  43396  sticksstones11  43398  sticksstones17  43405  sticksstones18  43406  aks6d1c6lem5  43419  mzpexpmpt  43949  mzpresrename  43954  diophrw  43963  rabren3dioph  44015  lnrfg  44313  seff  45485  sblpnf  45486  binomcxplemnotnn0  45532  stoweidlem44  47259  stirlinglem8  47296  fourierdlem62  47383  fouriersw  47446  nnsum3primes4  49091  grtriclwlk3  49248  zlmodzxzldeplem1  49817  aacllem  51219  amgmwlem  51267