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

Theorem fvssunirn 5911
Description: The result of a function value is always a subset of the union of the range, even if it is invalid and thus empty. (Contributed by Stefan O'Rear, 2-Nov-2014.) (Revised by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
fvssunirn  |-  ( F `
 X )  C_  U.
ran  F

Proof of Theorem fvssunirn
StepHypRef Expression
1 fvrn0 5910 . . 3  |-  ( F `
 X )  e.  ( ran  F  u.  {
(/) } )
2 elssuni 4241 . . 3  |-  ( ( F `  X )  e.  ( ran  F  u.  { (/) } )  -> 
( F `  X
)  C_  U. ( ran  F  u.  { (/) } ) )
31, 2ax-mp 5 . 2  |-  ( F `
 X )  C_  U. ( ran  F  u.  {
(/) } )
4 uniun 4231 . . 3  |-  U. ( ran  F  u.  { (/) } )  =  ( U. ran  F  u.  U. { (/)
} )
5 0ex 4549 . . . . 5  |-  (/)  e.  _V
65unisn 4227 . . . 4  |-  U. { (/)
}  =  (/)
76uneq2i 3597 . . 3  |-  ( U. ran  F  u.  U. { (/)
} )  =  ( U. ran  F  u.  (/) )
8 un0 3771 . . 3  |-  ( U. ran  F  u.  (/) )  = 
U. ran  F
94, 7, 83eqtri 2488 . 2  |-  U. ( ran  F  u.  { (/) } )  =  U. ran  F
103, 9sseqtri 3476 1  |-  ( F `
 X )  C_  U.
ran  F
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1898    u. cun 3414    C_ wss 3416   (/)c0 3743   {csn 3980   U.cuni 4212   ran crn 4854   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-cnv 4861  df-dm 4863  df-rn 4864  df-iota 5565  df-fv 5609
This theorem is referenced by:  ovssunirn  6344  marypha2lem1  7975  acnlem  8505  fin23lem29  8797  itunitc  8877  hsmexlem5  8886  wunfv  9183  wunex2  9189  strfvss  15188  prdsval  15402  prdsbas  15404  prdsplusg  15405  prdsmulr  15406  prdsvsca  15407  prdshom  15414  mreunirn  15556  mrcfval  15563  mrcssv  15569  mrisval  15585  sscpwex  15769  wunfunc  15853  catcxpccl  16141  comppfsc  20596  filunirn  20946  elflim  21035  flffval  21053  fclsval  21072  isfcls  21073  fcfval  21097  tsmsxplem1  21216  xmetunirn  21401  mopnval  21502  tmsval  21545  cfilfval  22283  caufval  22294  issgon  28994  elrnsiga  28997  volmeas  29103  omssubadd  29177  omssubaddOLD  29181  neibastop2lem  31065  ismtyval  32177  dicval  34789  ismrc  35588  nacsfix  35599  hbt  36034
  Copyright terms: Public domain W3C validator