MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fss Structured version   Visualization version   GIF version

Theorem fss 6521
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
StepHypRef Expression
1 sstr2 3973 . . . . 5 (ran 𝐹𝐵 → (𝐵𝐶 → ran 𝐹𝐶))
21com12 32 . . . 4 (𝐵𝐶 → (ran 𝐹𝐵 → ran 𝐹𝐶))
32anim2d 611 . . 3 (𝐵𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶)))
4 df-f 6353 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
5 df-f 6353 . . 3 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
63, 4, 53imtr4g 297 . 2 (𝐵𝐶 → (𝐹:𝐴𝐵𝐹:𝐴𝐶))
76impcom 408 1 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wss 3935  ran crn 5550   Fn wfn 6344  wf 6345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951  df-f 6353
This theorem is referenced by:  fssd  6522  f1ss  6574  frnssb  6878  fsn2  6891  fprb  6949  ofco  7418  ffoss  7638  issmo2  7977  smoiso  7990  ssdomg  8544  alephfplem4  9522  cofsmo  9680  fin23lem17  9749  hsmexlem1  9837  axdc3lem4  9864  ac6s  9895  gruen  10223  intgru  10225  ingru  10226  hashf1lem1  13803  sswrd  13859  wrdvOLD  13868  repsdf2  14130  limsupgre  14828  abscn2  14945  recn2  14947  imcn2  14948  climabs  14950  climre  14952  climim  14953  rlimabs  14955  rlimre  14957  rlimim  14958  caucvgrlem  15019  caurcvgr  15020  caucvgrlem2  15021  caurcvg  15023  fsumre  15153  fsumim  15154  0ram  16346  ramub1  16354  ramcl  16355  acsinfd  17780  acsdomd  17781  gsumval1  17883  resmhm2  17976  prdsgrpd  18149  prdsinvgd  18150  symgtrinv  18531  prdscmnd  18912  prdsabld  18913  pgpfaclem1  19134  prdsringd  19293  prdscrngd  19294  abvf  19525  prdslmodd  19672  psrridm  20114  coe1fval3  20306  zntoslem  20633  regsumsupp  20696  dsmmsubg  20817  dsmmlss  20818  islinds2  20887  lindsmm  20902  lsslindf  20904  1stccnp  22000  1stckgen  22092  prdstps  22167  pthaus  22176  txcmplem2  22180  ptcmpfi  22351  ptcmplem1  22590  ptcmpg  22595  prdstmdd  22661  prdstgpd  22662  ismet2  22872  prdsxmetlem  22907  imasdsf1olem  22912  prdsms  23070  isngp2  23135  metdscn  23393  lmmbr  23790  causs  23830  ovolfioo  23997  ovolficc  23998  ovolfsf  24001  elovolm  24005  ovollb  24009  ovolunlem1a  24026  ovolunlem1  24027  ovolicc2lem1  24047  ovolicc2lem2  24048  ovolicc2lem3  24049  ovolicc2lem4  24050  ovolicc2  24052  uniiccdif  24108  uniioovol  24109  uniiccvol  24110  uniioombllem2  24113  uniioombllem3a  24114  uniioombllem3  24115  uniioombllem4  24116  uniioombllem5  24117  uniioombl  24119  dyadmbl  24130  vitalilem3  24140  vitalilem4  24141  vitalilem5  24142  ismbf  24158  mbfid  24165  0plef  24202  i1f1  24220  i1faddlem  24223  i1fsub  24238  itg1sub  24239  mbfi1fseqlem4  24248  itg2le  24269  itg2mulclem  24276  itg2mulc  24277  itg2monolem1  24280  itg2monolem2  24281  itg2monolem3  24282  itg2mono  24283  itg2i1fseq3  24287  itg2addlem  24288  itg2gt0  24290  itg2cnlem1  24291  itg2cnlem2  24292  dvfre  24477  dvnfre  24478  dvferm1  24511  dvferm2  24513  rolle  24516  dvgt0lem1  24528  dvivthlem1  24534  dvne0  24537  lhop1lem  24539  lhop2  24541  lhop  24542  dvcnvrelem1  24543  dvcnvre  24545  dvcvx  24546  dvfsumrlim  24557  tdeglem3  24582  elplyr  24720  taylthlem2  24891  taylth  24892  ulmcn  24916  iblulm  24924  efcvx  24966  dvrelog  25147  relogcn  25148  dvlog2  25163  leibpi  25448  efrlim  25475  jensenlem2  25493  jensen  25494  amgmlem  25495  amgm  25496  wilthlem2  25574  wilthlem3  25575  basellem7  25592  basellem9  25594  lgsfcl  25809  lgsdchr  25859  dchrvmasumlem1  25999  dchrisum0lem3  26023  axlowdimlem4  26659  axlowdimlem7  26662  axlowdimlem10  26665  upgruhgr  26815  konigsbergssiedgw  27957  pliguhgr  28191  0oo  28494  hhsscms  28983  nlelchi  29766  hmopidmchi  29856  pjinvari  29896  padct  30382  smatrcl  30961  lmlim  31090  rge0scvg  31092  lmdvg  31096  lmdvglim  31097  rrhre  31162  esumfsupre  31230  hashf2  31243  eulerpartlems  31518  eulerpartlemgs2  31538  coinfliprv  31640  fdvposlt  31770  fdvposle  31772  breprexpnat  31805  circlemethnat  31812  circlevma  31813  tgoldbachgtde  31831  lfuhgr  32262  subgrwlk  32277  ptpconn  32378  poimirlem8  34782  poimirlem18  34792  poimirlem21  34795  poimirlem22  34796  mblfinlem2  34812  mbfresfi  34820  itg2addnclem  34825  itg2addnclem2  34826  itg2addnc  34828  itg2gt0cn  34829  ftc1anclem8  34856  fdc  34903  heiborlem6  34977  heibor  34982  lfl0f  36087  mzpexpmpt  39222  mzpresrename  39227  diophrw  39236  rabren3dioph  39292  lnrfg  39599  seff  40521  sblpnf  40522  binomcxplemnotnn0  40568  stoweidlem44  42210  stirlinglem8  42247  fourierdlem62  42334  fouriersw  42397  nnsum3primes4  43800  resmgmhm2  43913  zlmodzxzldeplem1  44453  aacllem  44800  amgmwlem  44801
  Copyright terms: Public domain W3C validator