Theorem fss 6613

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3891  ran crn 5589   Fn wfn 6425  ⟶wf 6426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908  df-f 6434

This theorem is referenced by:  fssd  6614  f1ss  6672  frnssb  6989  fsn2  7002  fprb  7063  ofco  7547  ffoss  7775  issmo2  8164  smoiso  8177  ssdomg  8757  alephfplem4  9847  cofsmo  10009  fin23lem17  10078  hsmexlem1  10166  axdc3lem4  10193  ac6s  10224  gruen  10552  intgru  10554  ingru  10555  hashf1lem1  14149  hashf1lem1OLD  14150  sswrd  14206  repsdf2  14472  limsupgre  15171  abscn2  15289  recn2  15291  imcn2  15292  climabs  15294  climre  15296  climim  15297  rlimabs  15299  rlimre  15301  rlimim  15302  caucvgrlem  15365  caurcvgr  15366  caucvgrlem2  15367  caurcvg  15369  fsumre  15501  fsumim  15502  0ram  16702  ramub1  16710  ramcl  16711  acsinfd  18255  acsdomd  18256  gsumval1  18348  resmhm2  18441  prdsgrpd  18666  prdsinvgd  18667  symgtrinv  19061  prdscmnd  19443  prdsabld  19444  pgpfaclem1  19665  prdsringd  19832  prdscrngd  19833  abvf  20064  prdslmodd  20212  zntoslem  20745  regsumsupp  20808  dsmmsubg  20931  dsmmlss  20932  islinds2  21001  lindsmm  21016  lsslindf  21018  psrridm  21154  coe1fval3  21360  1stccnp  22594  1stckgen  22686  prdstps  22761  pthaus  22770  txcmplem2  22774  ptcmpfi  22945  ptcmplem1  23184  ptcmpg  23189  prdstmdd  23256  prdstgpd  23257  ismet2  23467  prdsxmetlem  23502  imasdsf1olem  23507  prdsms  23668  isngp2  23734  metdscn  24000  lmmbr  24403  causs  24443  ovolfioo  24612  ovolficc  24613  ovolfsf  24616  elovolm  24620  ovollb  24624  ovolunlem1a  24641  ovolunlem1  24642  ovolicc2lem1  24662  ovolicc2lem2  24663  ovolicc2lem3  24664  ovolicc2lem4  24665  ovolicc2  24667  uniiccdif  24723  uniioovol  24724  uniiccvol  24725  uniioombllem2  24728  uniioombllem3a  24729  uniioombllem3  24730  uniioombllem4  24731  uniioombllem5  24732  uniioombl  24734  dyadmbl  24745  vitalilem3  24755  vitalilem4  24756  vitalilem5  24757  ismbf  24773  mbfid  24780  0plef  24817  i1f1  24835  i1faddlem  24838  i1fsub  24854  itg1sub  24855  mbfi1fseqlem4  24864  itg2le  24885  itg2mulclem  24892  itg2mulc  24893  itg2monolem1  24896  itg2monolem2  24897  itg2monolem3  24898  itg2mono  24899  itg2i1fseq3  24903  itg2addlem  24904  itg2gt0  24906  itg2cnlem1  24907  itg2cnlem2  24908  dvfre  25096  dvnfre  25097  dvferm1  25130  dvferm2  25132  rolle  25135  dvgt0lem1  25147  dvivthlem1  25153  dvne0  25156  lhop1lem  25158  lhop2  25160  lhop  25161  dvcnvrelem1  25162  dvcnvre  25164  dvcvx  25165  dvfsumrlim  25176  tdeglem3  25203  tdeglem3OLD  25204  elplyr  25343  taylthlem2  25514  taylth  25515  ulmcn  25539  iblulm  25547  efcvx  25589  dvrelog  25773  relogcn  25774  dvlog2  25789  leibpi  26073  efrlim  26100  jensenlem2  26118  jensen  26119  amgmlem  26120  amgm  26121  wilthlem2  26199  wilthlem3  26200  basellem7  26217  basellem9  26219  lgsfcl  26434  lgsdchr  26484  dchrvmasumlem1  26624  dchrisum0lem3  26648  axlowdimlem4  27294  axlowdimlem7  27297  axlowdimlem10  27300  upgruhgr  27453  konigsbergssiedgw  28593  pliguhgr  28827  0oo  29130  hhsscms  29619  nlelchi  30402  hmopidmchi  30492  pjinvari  30532  padct  31033  smatrcl  31725  lmlim  31876  rge0scvg  31878  lmdvg  31882  lmdvglim  31883  rrhre  31950  esumfsupre  32018  hashf2  32031  eulerpartlems  32306  eulerpartlemgs2  32326  coinfliprv  32428  fdvposlt  32558  fdvposle  32560  breprexpnat  32593  circlemethnat  32600  circlevma  32601  tgoldbachgtde  32619  lfuhgr  33058  subgrwlk  33073  ptpconn  33174  poimirlem8  35764  poimirlem18  35774  poimirlem21  35777  poimirlem22  35778  mblfinlem2  35794  mbfresfi  35802  itg2addnclem  35807  itg2addnclem2  35808  itg2addnc  35810  itg2gt0cn  35811  ftc1anclem8  35836  fdc  35882  heiborlem6  35953  heibor  35958  lfl0f  37062  intlewftc  40049  sticksstones3  40084  sticksstones9  40090  sticksstones11  40092  sticksstones17  40099  sticksstones18  40100  mzpexpmpt  40547  mzpresrename  40552  diophrw  40561  rabren3dioph  40617  lnrfg  40924  seff  41880  sblpnf  41881  binomcxplemnotnn0  41927  stoweidlem44  43539  stirlinglem8  43576  fourierdlem62  43663  fouriersw  43726  nnsum3primes4  45192  resmgmhm2  45305  zlmodzxzldeplem1  45793  aacllem  46457  amgmwlem  46458