Theorem fss 6526

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 3973	. . . . 5 ⊢ (ran 𝐹 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → ran 𝐹 ⊆ 𝐶))
2	1	com12 32	. . . 4 ⊢ (𝐵 ⊆ 𝐶 → (ran 𝐹 ⊆ 𝐵 → ran 𝐹 ⊆ 𝐶))
3	2	anim2d 613	. . 3 ⊢ (𝐵 ⊆ 𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶)))
4		df-f 6358	. . 3 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
5		df-f 6358	. . 3 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
6	3, 4, 5	3imtr4g 298	. 2 ⊢ (𝐵 ⊆ 𝐶 → (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶𝐶))
7	6	impcom 410	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3935  ran crn 5555   Fn wfn 6349  ⟶wf 6350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951  df-f 6358

This theorem is referenced by:  fssd  6527  f1ss  6579  frnssb  6884  fsn2  6897  fprb  6955  ofco  7428  ffoss  7646  issmo2  7985  smoiso  7998  ssdomg  8554  alephfplem4  9532  cofsmo  9690  fin23lem17  9759  hsmexlem1  9847  axdc3lem4  9874  ac6s  9905  gruen  10233  intgru  10235  ingru  10236  hashf1lem1  13812  sswrd  13868  wrdvOLD  13877  repsdf2  14139  limsupgre  14837  abscn2  14954  recn2  14956  imcn2  14957  climabs  14959  climre  14961  climim  14962  rlimabs  14964  rlimre  14966  rlimim  14967  caucvgrlem  15028  caurcvgr  15029  caucvgrlem2  15030  caurcvg  15032  fsumre  15162  fsumim  15163  0ram  16355  ramub1  16363  ramcl  16364  acsinfd  17789  acsdomd  17790  gsumval1  17892  resmhm2  17985  prdsgrpd  18208  prdsinvgd  18209  symgtrinv  18599  prdscmnd  18980  prdsabld  18981  pgpfaclem1  19202  prdsringd  19361  prdscrngd  19362  abvf  19593  prdslmodd  19740  psrridm  20183  coe1fval3  20375  zntoslem  20702  regsumsupp  20765  dsmmsubg  20886  dsmmlss  20887  islinds2  20956  lindsmm  20971  lsslindf  20973  1stccnp  22069  1stckgen  22161  prdstps  22236  pthaus  22245  txcmplem2  22249  ptcmpfi  22420  ptcmplem1  22659  ptcmpg  22664  prdstmdd  22731  prdstgpd  22732  ismet2  22942  prdsxmetlem  22977  imasdsf1olem  22982  prdsms  23140  isngp2  23205  metdscn  23463  lmmbr  23860  causs  23900  ovolfioo  24067  ovolficc  24068  ovolfsf  24071  elovolm  24075  ovollb  24079  ovolunlem1a  24096  ovolunlem1  24097  ovolicc2lem1  24117  ovolicc2lem2  24118  ovolicc2lem3  24119  ovolicc2lem4  24120  ovolicc2  24122  uniiccdif  24178  uniioovol  24179  uniiccvol  24180  uniioombllem2  24183  uniioombllem3a  24184  uniioombllem3  24185  uniioombllem4  24186  uniioombllem5  24187  uniioombl  24189  dyadmbl  24200  vitalilem3  24210  vitalilem4  24211  vitalilem5  24212  ismbf  24228  mbfid  24235  0plef  24272  i1f1  24290  i1faddlem  24293  i1fsub  24308  itg1sub  24309  mbfi1fseqlem4  24318  itg2le  24339  itg2mulclem  24346  itg2mulc  24347  itg2monolem1  24350  itg2monolem2  24351  itg2monolem3  24352  itg2mono  24353  itg2i1fseq3  24357  itg2addlem  24358  itg2gt0  24360  itg2cnlem1  24361  itg2cnlem2  24362  dvfre  24547  dvnfre  24548  dvferm1  24581  dvferm2  24583  rolle  24586  dvgt0lem1  24598  dvivthlem1  24604  dvne0  24607  lhop1lem  24609  lhop2  24611  lhop  24612  dvcnvrelem1  24613  dvcnvre  24615  dvcvx  24616  dvfsumrlim  24627  tdeglem3  24652  elplyr  24790  taylthlem2  24961  taylth  24962  ulmcn  24986  iblulm  24994  efcvx  25036  dvrelog  25219  relogcn  25220  dvlog2  25235  leibpi  25519  efrlim  25546  jensenlem2  25564  jensen  25565  amgmlem  25566  amgm  25567  wilthlem2  25645  wilthlem3  25646  basellem7  25663  basellem9  25665  lgsfcl  25880  lgsdchr  25930  dchrvmasumlem1  26070  dchrisum0lem3  26094  axlowdimlem4  26730  axlowdimlem7  26733  axlowdimlem10  26736  upgruhgr  26886  konigsbergssiedgw  28028  pliguhgr  28262  0oo  28565  hhsscms  29054  nlelchi  29837  hmopidmchi  29927  pjinvari  29967  padct  30454  smatrcl  31061  lmlim  31190  rge0scvg  31192  lmdvg  31196  lmdvglim  31197  rrhre  31262  esumfsupre  31330  hashf2  31343  eulerpartlems  31618  eulerpartlemgs2  31638  coinfliprv  31740  fdvposlt  31870  fdvposle  31872  breprexpnat  31905  circlemethnat  31912  circlevma  31913  tgoldbachgtde  31931  lfuhgr  32364  subgrwlk  32379  ptpconn  32480  poimirlem8  34899  poimirlem18  34909  poimirlem21  34912  poimirlem22  34913  mblfinlem2  34929  mbfresfi  34937  itg2addnclem  34942  itg2addnclem2  34943  itg2addnc  34945  itg2gt0cn  34946  ftc1anclem8  34973  fdc  35019  heiborlem6  35093  heibor  35098  lfl0f  36204  mzpexpmpt  39340  mzpresrename  39345  diophrw  39354  rabren3dioph  39410  lnrfg  39717  seff  40639  sblpnf  40640  binomcxplemnotnn0  40686  stoweidlem44  42328  stirlinglem8  42365  fourierdlem62  42452  fouriersw  42515  nnsum3primes4  43952  resmgmhm2  44065  zlmodzxzldeplem1  44554  aacllem  44901  amgmwlem  44902