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

Theorem fvssunirn 5589
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 5588 . . 3  |-  ( F `
 X )  e.  ( ran  F  u.  {
(/) } )
2 elssuni 3892 . . 3  |-  ( ( F `  X )  e.  ( ran  F  u.  { (/) } )  -> 
( F `  X
)  C_  U. ( ran  F  u.  { (/) } ) )
31, 2ax-mp 8 . 2  |-  ( F `
 X )  C_  U. ( ran  F  u.  {
(/) } )
4 uniun 3883 . . 3  |-  U. ( ran  F  u.  { (/) } )  =  ( U. ran  F  u.  U. { (/)
} )
5 0ex 4187 . . . . 5  |-  (/)  e.  _V
65unisn 3880 . . . 4  |-  U. { (/)
}  =  (/)
76uneq2i 3360 . . 3  |-  ( U. ran  F  u.  U. { (/)
} )  =  ( U. ran  F  u.  (/) )
8 un0 3513 . . 3  |-  ( U. ran  F  u.  (/) )  = 
U. ran  F
94, 7, 83eqtri 2340 . 2  |-  U. ( ran  F  u.  { (/) } )  =  U. ran  F
103, 9sseqtri 3244 1  |-  ( F `
 X )  C_  U.
ran  F
Colors of variables: wff set class
Syntax hints:    e. wcel 1701    u. cun 3184    C_ wss 3186   (/)c0 3489   {csn 3674   U.cuni 3864   ran crn 4727   ` cfv 5292
This theorem is referenced by:  ovssunirn  5926  marypha2lem1  7233  acnlem  7720  fin23lem29  8012  itunitc  8092  hsmexlem5  8101  wunfv  8399  wunex2  8405  strfvss  13213  prdsval  13404  prdsbas  13406  prdsplusg  13407  prdsmulr  13408  prdsvsca  13409  prdshom  13415  mreunirn  13552  mrcfval  13559  mrcssv  13565  mrisval  13581  sscpwex  13741  wunfunc  13822  catcxpccl  14030  filunirn  17629  elflim  17718  flffval  17736  fclsval  17755  isfcls  17756  fcfval  17780  tsmsxplem1  17887  xmetunirn  17954  blfval  17999  mopnval  18036  tmsval  18079  cfilfval  18743  caufval  18754  issgon  23682  elrnsiga  23685  volmeas  23761  comppfsc  25456  neibastop2lem  25458  ismtyval  25672  ismrc  25924  nacsfix  25935  hbt  26482  dicval  31184
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-sbc 3026  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-cnv 4734  df-dm 4736  df-rn 4737  df-iota 5256  df-fv 5300
  Copyright terms: Public domain W3C validator