Theorem fss 6723

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 3941	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 33	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 624	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6541	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6541	. . 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 3902  ran crn 5660   Fn wfn 6532  ⟶wf 6533

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 3919  df-f 6541

This theorem is used by:  fssd  6724  f1ss  6782  fcdmssb  7119  fsn2  7134  fprb  7196  ofco  7707  ffoss  7947  issmo2  8342  smoiso  8355  ssdomg  9010  alephfplem4  10114  cofsmo  10275  fin23lem17  10344  hsmexlem1  10432  axdc3lem4  10459  ac6s  10490  gruen  10825  intgru  10827  ingru  10828  hashf1lem1  14524  sswrd  14591  repsdf2  14853  limsupgre  15572  abscn2  15690  recn2  15692  imcn2  15693  climabs  15695  climre  15697  climim  15698  rlimabs  15700  rlimre  15702  rlimim  15703  caucvgrlem  15764  caurcvgr  15765  caucvgrlem2  15766  caurcvg  15768  fsumre  15899  fsumim  15900  0ram  17118  ramub1  17126  ramcl  17127  acsinfd  18650  acsdomd  18651  gsumval1  18791  resmgmhm2  18820  resmhm2  18936  prdsgrpd  19179  prdsinvgd  19180  symgtrinv  19605  prdscmnd  19994  prdsabld  19995  pgpfaclem1  20216  prdsrngd  20317  prdsmulrcl  20466  prdsringd  20467  prdscrngd  20468  abvf  20987  prdslmodd  21159  zntoslem  21775  regsumsupp  21841  dsmmsubg  21962  dsmmlss  21963  islinds2  22032  lindsmm  22047  lsslindf  22049  psrridm  22183  coe1fval3  22439  1stccnp  23694  1stckgen  23786  prdstps  23861  pthaus  23870  txcmplem2  23874  ptcmpfi  24045  ptcmplem1  24284  ptcmpg  24289  prdstmdd  24356  prdstgpd  24357  ismet2  24565  prdsxmetlem  24600  imasdsf1olem  24605  prdsms  24763  isngp2  24829  metdscn  25089  lmmbr  25492  causs  25532  ovolfioo  25701  ovolficc  25702  ovolfsf  25705  elovolm  25709  ovollb  25713  ovolunlem1a  25730  ovolunlem1  25731  ovolicc2lem1  25751  ovolicc2lem2  25752  ovolicc2lem3  25753  ovolicc2lem4  25754  ovolicc2  25756  uniiccdif  25812  uniioovol  25813  uniiccvol  25814  uniioombllem2  25817  uniioombllem3a  25818  uniioombllem3  25819  uniioombllem4  25820  uniioombllem5  25821  uniioombl  25823  dyadmbl  25834  vitalilem3  25844  vitalilem4  25845  vitalilem5  25846  ismbf  25862  mbfid  25869  0plef  25906  i1f1  25924  i1faddlem  25927  i1fsub  25942  itg1sub  25943  mbfi1fseqlem4  25952  itg2le  25973  itg2mulclem  25980  itg2mulc  25981  itg2monolem1  25984  itg2monolem2  25985  itg2monolem3  25986  itg2mono  25987  itg2i1fseq3  25991  itg2addlem  25992  itg2gt0  25994  itg2cnlem1  25995  itg2cnlem2  25996  dvfre  26185  dvnfre  26186  dvferm1  26219  dvferm2  26221  rolle  26224  dvgt0lem1  26236  dvivthlem1  26242  dvne0  26245  lhop1lem  26247  lhop2  26249  lhop  26250  dvcnvrelem1  26251  dvcnvre  26253  dvcvx  26254  dvfsumrlim  26265  tdeglem3  26291  elplyr  26433  taylthlem2  26617  taylth  26618  ulmcn  26642  iblulm  26650  efcvx  26692  dvrelog  26882  relogcn  26883  dvlog2  26898  leibpi  27187  efrlim  27214  jensenlem2  27232  jensen  27233  amgmlem  27234  amgm  27235  wilthlem2  27313  wilthlem3  27314  basellem7  27331  basellem9  27333  lgsfcl  27549  lgsdchr  27599  dchrvmasumlem1  27739  dchrisum0lem3  27763  axlowdimlem4  29410  axlowdimlem7  29413  axlowdimlem10  29416  upgruhgr  29567  lfuhgr  29613  subgrwlk  30156  konigsbergssiedgw  30738  pliguhgr  30975  0oo  31278  hhsscms  31767  nlelchi  32550  hmopidmchi  32640  pjinvari  32680  padct  33197  smatrcl  34314  lmlim  34465  rge0scvg  34467  lmdvg  34471  lmdvglim  34472  rrhre  34539  esumfsupre  34589  hashf2  34602  eulerpartlems  34879  eulerpartlemgs2  34899  coinfliprv  35002  fdvposlt  35115  fdvposle  35117  breprexpnat  35150  circlemethnat  35157  circlevma  35158  tgoldbachgtde  35176  ptpconn  35820  poimirlem8  38385  poimirlem18  38395  poimirlem21  38398  poimirlem22  38399  mblfinlem2  38415  mbfresfi  38423  itg2addnclem  38428  itg2addnclem2  38429  itg2addnc  38431  itg2gt0cn  38432  ftc1anclem8  38457  fdc  38503  heiborlem6  38574  heibor  38579  lfl0f  39950  intlewftc  42935  sticksstones3  43022  sticksstones9  43028  sticksstones11  43030  sticksstones17  43037  sticksstones18  43038  aks6d1c6lem5  43051  mzpexpmpt  43598  mzpresrename  43603  diophrw  43612  rabren3dioph  43664  lnrfg  43968  seff  45141  sblpnf  45142  binomcxplemnotnn0  45188  stoweidlem44  46880  stirlinglem8  46917  fourierdlem62  47004  fouriersw  47067  nnsum3primes4  48712  grtriclwlk3  48869  zlmodzxzldeplem1  49438  aacllem  50780  amgmwlem  50828