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

Theorem fss 6094
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 3643 . . . . 5 (ran 𝐹𝐵 → (𝐵𝐶 → ran 𝐹𝐶))
21com12 32 . . . 4 (𝐵𝐶 → (ran 𝐹𝐵 → ran 𝐹𝐶))
32anim2d 588 . . 3 (𝐵𝐶 → ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐵) → (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶)))
4 df-f 5930 . . 3 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
5 df-f 5930 . . 3 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
63, 4, 53imtr4g 285 . 2 (𝐵𝐶 → (𝐹:𝐴𝐵𝐹:𝐴𝐶))
76impcom 445 1 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wss 3607  ran crn 5144   Fn wfn 5921  wf 5922
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621  df-f 5930
This theorem is referenced by:  fssd  6095  f1ss  6144  frnssb  6431  fsn2  6443  fsnex  6578  ofco  6959  ffoss  7169  issmo2  7491  smoiso  7504  mapsn  7941  ssdomg  8043  alephfplem4  8968  cofsmo  9129  fin23lem17  9198  hsmexlem1  9286  axdc3lem4  9313  ac6s  9344  gruen  9672  intgru  9674  ingru  9675  hashf1lem1  13277  sswrd  13345  wrdv  13352  repsdf2  13571  limsupgre  14256  abscn2  14373  recn2  14375  imcn2  14376  climabs  14378  climre  14380  climim  14381  rlimabs  14383  rlimre  14385  rlimim  14386  caucvgrlem  14447  caurcvgr  14448  caucvgrlem2  14449  caurcvg  14451  fsumre  14584  fsumim  14585  0ram  15771  ramub1  15779  ramcl  15780  acsinfd  17227  acsdomd  17228  gsumval1  17324  resmhm2  17407  prdsgrpd  17572  prdsinvgd  17573  symgtrinv  17938  prdscmnd  18310  prdsabld  18311  pgpfaclem1  18526  prdsringd  18658  prdscrngd  18659  abvf  18871  prdslmodd  19017  psrridm  19452  coe1fval3  19626  zntoslem  19953  regsumsupp  20016  dsmmsubg  20135  dsmmlss  20136  islinds2  20200  lindsmm  20215  lsslindf  20217  1stccnp  21313  1stckgen  21405  prdstps  21480  pthaus  21489  txcmplem2  21493  ptcmpfi  21664  ptcmplem1  21903  ptcmpg  21908  prdstmdd  21974  prdstgpd  21975  ismet2  22185  prdsxmetlem  22220  imasdsf1olem  22225  prdsms  22383  isngp2  22448  metdscn  22706  lmmbr  23102  causs  23142  ovolfioo  23282  ovolficc  23283  ovolfsf  23286  elovolm  23289  ovollb  23293  ovolunlem1a  23310  ovolunlem1  23311  ovolicc2lem1  23331  ovolicc2lem2  23332  ovolicc2lem3  23333  ovolicc2lem4  23334  ovolicc2  23336  uniiccdif  23392  uniioovol  23393  uniiccvol  23394  uniioombllem2  23397  uniioombllem3a  23398  uniioombllem3  23399  uniioombllem4  23400  uniioombllem5  23401  uniioombl  23403  dyadmbl  23414  vitalilem3  23424  vitalilem4  23425  vitalilem5  23426  ismbf  23442  mbfid  23448  0plef  23484  i1f1  23502  i1faddlem  23505  i1fsub  23520  itg1sub  23521  mbfi1fseqlem4  23530  itg2le  23551  itg2mulclem  23558  itg2mulc  23559  itg2monolem1  23562  itg2monolem2  23563  itg2monolem3  23564  itg2mono  23565  itg2i1fseqle  23566  itg2i1fseq3  23569  itg2addlem  23570  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  dvfre  23759  dvnfre  23760  dvferm1  23793  dvferm2  23795  rolle  23798  dvgt0lem1  23810  dvivthlem1  23816  dvne0  23819  lhop1lem  23821  lhop2  23823  lhop  23824  dvcnvrelem1  23825  dvcnvre  23827  dvcvx  23828  dvfsumrlim  23839  tdeglem3  23864  elplyr  24002  taylthlem2  24173  taylth  24174  ulmcn  24198  iblulm  24206  efcvx  24248  dvrelog  24428  relogcn  24429  dvlog2  24444  leibpi  24714  efrlim  24741  jensenlem2  24759  jensen  24760  amgmlem  24761  amgm  24762  wilthlem2  24840  wilthlem3  24841  basellem7  24858  basellem9  24860  lgsfcl  25075  lgsdchr  25125  dchrvmasumlem1  25229  dchrisum0lem3  25253  axlowdimlem4  25870  axlowdimlem7  25873  axlowdimlem10  25876  upgruhgr  26042  konigsbergssiedgw  27228  pliguhgr  27468  0oo  27772  hhsscms  28264  nlelchi  29048  hmopidmchi  29138  pjinvari  29178  padct  29625  smatrcl  29990  lmlim  30121  rge0scvg  30123  lmdvg  30127  lmdvglim  30128  rrhre  30193  esumfsupre  30261  hashf2  30274  eulerpartlems  30550  eulerpartlemgs2  30570  coinfliprv  30672  fdvposlt  30805  fdvposle  30807  breprexpnat  30840  circlemethnat  30847  circlevma  30848  tgoldbachgtde  30866  ptpconn  31341  fprb  31795  poimirlem8  33547  poimirlem18  33557  poimirlem21  33560  poimirlem22  33561  mblfinlem2  33577  mbfresfi  33586  itg2addnclem  33591  itg2addnclem2  33592  itg2addnc  33594  itg2gt0cn  33595  ftc1anclem8  33622  fdc  33671  heiborlem6  33745  heibor  33750  lfl0f  34674  mzpexpmpt  37625  mzpresrename  37630  diophrw  37639  rabren3dioph  37696  lnrfg  38006  seff  38825  sblpnf  38826  binomcxplemnotnn0  38872  mapsnd  39702  stoweidlem44  40579  stirlinglem8  40616  fourierdlem62  40703  fouriersw  40766  nnsum3primes4  42001  resmgmhm2  42124  zlmodzxzldeplem1  42614  aacllem  42875  amgmwlem  42876
  Copyright terms: Public domain W3C validator