Theorem fss 6752

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

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3962  ran crn 5689   Fn wfn 6557  ⟶wf 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3979  df-f 6566

This theorem is referenced by:  fssd  6753  f1ss  6809  fcdmssb  7141  fsn2  7155  fprb  7213  ofco  7721  ffoss  7968  issmo2  8387  smoiso  8400  ssdomg  9038  alephfplem4  10144  cofsmo  10306  fin23lem17  10375  hsmexlem1  10463  axdc3lem4  10490  ac6s  10521  gruen  10849  intgru  10851  ingru  10852  hashf1lem1  14490  sswrd  14556  repsdf2  14812  limsupgre  15513  abscn2  15631  recn2  15633  imcn2  15634  climabs  15636  climre  15638  climim  15639  rlimabs  15641  rlimre  15643  rlimim  15644  caucvgrlem  15705  caurcvgr  15706  caucvgrlem2  15707  caurcvg  15709  fsumre  15840  fsumim  15841  0ram  17053  ramub1  17061  ramcl  17062  acsinfd  18613  acsdomd  18614  gsumval1  18708  resmgmhm2  18737  resmhm2  18846  prdsgrpd  19080  prdsinvgd  19081  symgtrinv  19504  prdscmnd  19893  prdsabld  19894  pgpfaclem1  20115  prdsrngd  20193  prdsmulrcl  20333  prdsringd  20334  prdscrngd  20335  abvf  20832  prdslmodd  20984  zntoslem  21592  regsumsupp  21657  dsmmsubg  21780  dsmmlss  21781  islinds2  21850  lindsmm  21865  lsslindf  21867  psrridm  22000  coe1fval3  22225  1stccnp  23485  1stckgen  23577  prdstps  23652  pthaus  23661  txcmplem2  23665  ptcmpfi  23836  ptcmplem1  24075  ptcmpg  24080  prdstmdd  24147  prdstgpd  24148  ismet2  24358  prdsxmetlem  24393  imasdsf1olem  24398  prdsms  24559  isngp2  24625  metdscn  24891  lmmbr  25305  causs  25345  ovolfioo  25515  ovolficc  25516  ovolfsf  25519  elovolm  25523  ovollb  25527  ovolunlem1a  25544  ovolunlem1  25545  ovolicc2lem1  25565  ovolicc2lem2  25566  ovolicc2lem3  25567  ovolicc2lem4  25568  ovolicc2  25570  uniiccdif  25626  uniioovol  25627  uniiccvol  25628  uniioombllem2  25631  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  uniioombl  25637  dyadmbl  25648  vitalilem3  25658  vitalilem4  25659  vitalilem5  25660  ismbf  25676  mbfid  25683  0plef  25720  i1f1  25738  i1faddlem  25741  i1fsub  25757  itg1sub  25758  mbfi1fseqlem4  25767  itg2le  25788  itg2mulclem  25795  itg2mulc  25796  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2i1fseq3  25806  itg2addlem  25807  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  dvfre  26003  dvnfre  26004  dvferm1  26037  dvferm2  26039  rolle  26042  dvgt0lem1  26055  dvivthlem1  26061  dvne0  26064  lhop1lem  26066  lhop2  26068  lhop  26069  dvcnvrelem1  26070  dvcnvre  26072  dvcvx  26073  dvfsumrlim  26086  tdeglem3  26112  elplyr  26254  taylthlem2  26430  taylthlem2OLD  26431  taylth  26432  ulmcn  26456  iblulm  26464  efcvx  26507  dvrelog  26693  relogcn  26694  dvlog2  26709  leibpi  26999  efrlim  27026  efrlimOLD  27027  jensenlem2  27045  jensen  27046  amgmlem  27047  amgm  27048  wilthlem2  27126  wilthlem3  27127  basellem7  27144  basellem9  27146  lgsfcl  27363  lgsdchr  27413  dchrvmasumlem1  27553  dchrisum0lem3  27577  axlowdimlem4  28974  axlowdimlem7  28977  axlowdimlem10  28980  upgruhgr  29133  konigsbergssiedgw  30278  pliguhgr  30514  0oo  30817  hhsscms  31306  nlelchi  32089  hmopidmchi  32179  pjinvari  32219  padct  32736  smatrcl  33756  lmlim  33907  rge0scvg  33909  lmdvg  33913  lmdvglim  33914  rrhre  33983  esumfsupre  34051  hashf2  34064  eulerpartlems  34341  eulerpartlemgs2  34361  coinfliprv  34463  fdvposlt  34592  fdvposle  34594  breprexpnat  34627  circlemethnat  34634  circlevma  34635  tgoldbachgtde  34653  lfuhgr  35101  subgrwlk  35116  ptpconn  35217  poimirlem8  37614  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  mblfinlem2  37644  mbfresfi  37652  itg2addnclem  37657  itg2addnclem2  37658  itg2addnc  37660  itg2gt0cn  37661  ftc1anclem8  37686  fdc  37731  heiborlem6  37802  heibor  37807  lfl0f  39050  intlewftc  42042  sticksstones3  42129  sticksstones9  42135  sticksstones11  42137  sticksstones17  42144  sticksstones18  42145  aks6d1c6lem5  42158  mzpexpmpt  42732  mzpresrename  42737  diophrw  42746  rabren3dioph  42802  lnrfg  43107  seff  44304  sblpnf  44305  binomcxplemnotnn0  44351  stoweidlem44  45999  stirlinglem8  46036  fourierdlem62  46123  fouriersw  46186  nnsum3primes4  47712  grtriclwlk3  47849  zlmodzxzldeplem1  48345  aacllem  49031  amgmwlem  49032