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

Theorem fvssunirn 5895
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 5894 . . 3  |-  ( F `
 X )  e.  ( ran  F  u.  {
(/) } )
2 elssuni 4242 . . 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 4232 . . 3  |-  U. ( ran  F  u.  { (/) } )  =  ( U. ran  F  u.  U. { (/)
} )
5 0ex 4548 . . . . 5  |-  (/)  e.  _V
65unisn 4228 . . . 4  |-  U. { (/)
}  =  (/)
76uneq2i 3614 . . 3  |-  ( U. ran  F  u.  U. { (/)
} )  =  ( U. ran  F  u.  (/) )
8 un0 3784 . . 3  |-  ( U. ran  F  u.  (/) )  = 
U. ran  F
94, 7, 83eqtri 2453 . 2  |-  U. ( ran  F  u.  { (/) } )  =  U. ran  F
103, 9sseqtri 3493 1  |-  ( F `
 X )  C_  U.
ran  F
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1867    u. cun 3431    C_ wss 3433   (/)c0 3758   {csn 3993   U.cuni 4213   ran crn 4846   ` cfv 5592
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-cnv 4853  df-dm 4855  df-rn 4856  df-iota 5556  df-fv 5600
This theorem is referenced by:  ovssunirn  6325  marypha2lem1  7946  acnlem  8468  fin23lem29  8760  itunitc  8840  hsmexlem5  8849  wunfv  9146  wunex2  9152  strfvss  15091  prdsval  15305  prdsbas  15307  prdsplusg  15308  prdsmulr  15309  prdsvsca  15310  prdshom  15317  mreunirn  15451  mrcfval  15458  mrcssv  15464  mrisval  15480  sscpwex  15664  wunfunc  15748  catcxpccl  16036  comppfsc  20471  filunirn  20821  elflim  20910  flffval  20928  fclsval  20947  isfcls  20948  fcfval  20972  tsmsxplem1  21091  xmetunirn  21276  mopnval  21377  tmsval  21420  cfilfval  22120  caufval  22131  issgon  28781  elrnsiga  28784  volmeas  28890  omssubadd  28958  neibastop2lem  30798  ismtyval  31836  dicval  34453  ismrc  35252  nacsfix  35263  hbt  35699
  Copyright terms: Public domain W3C validator