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

Theorem fvssunirn 5718
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 5717 . . 3  |-  ( F `
 X )  e.  ( ran  F  u.  {
(/) } )
2 elssuni 4126 . . 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 4115 . . 3  |-  U. ( ran  F  u.  { (/) } )  =  ( U. ran  F  u.  U. { (/)
} )
5 0ex 4427 . . . . 5  |-  (/)  e.  _V
65unisn 4111 . . . 4  |-  U. { (/)
}  =  (/)
76uneq2i 3512 . . 3  |-  ( U. ran  F  u.  U. { (/)
} )  =  ( U. ran  F  u.  (/) )
8 un0 3667 . . 3  |-  ( U. ran  F  u.  (/) )  = 
U. ran  F
94, 7, 83eqtri 2467 . 2  |-  U. ( ran  F  u.  { (/) } )  =  U. ran  F
103, 9sseqtri 3393 1  |-  ( F `
 X )  C_  U.
ran  F
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756    u. cun 3331    C_ wss 3333   (/)c0 3642   {csn 3882   U.cuni 4096   ran crn 4846   ` cfv 5423
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-rab 2729  df-v 2979  df-sbc 3192  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-nul 3643  df-if 3797  df-sn 3883  df-pr 3885  df-op 3889  df-uni 4097  df-br 4298  df-opab 4356  df-cnv 4853  df-dm 4855  df-rn 4856  df-iota 5386  df-fv 5431
This theorem is referenced by:  ovssunirn  6122  marypha2lem1  7690  acnlem  8223  fin23lem29  8515  itunitc  8595  hsmexlem5  8604  wunfv  8904  wunex2  8910  strfvss  14197  prdsval  14398  prdsbas  14400  prdsplusg  14401  prdsmulr  14402  prdsvsca  14403  prdshom  14410  mreunirn  14544  mrcfval  14551  mrcssv  14557  mrisval  14573  sscpwex  14733  wunfunc  14814  catcxpccl  15022  filunirn  19460  elflim  19549  flffval  19567  fclsval  19586  isfcls  19587  fcfval  19611  tsmsxplem1  19732  xmetunirn  19917  mopnval  20018  tmsval  20061  cfilfval  20780  caufval  20791  issgon  26571  elrnsiga  26574  volmeas  26652  comppfsc  28584  neibastop2lem  28586  ismtyval  28704  ismrc  29042  nacsfix  29053  hbt  29491  dicval  34826
  Copyright terms: Public domain W3C validator