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

Theorem fvssunirn 6692
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 (𝐹𝑋) ⊆ ran 𝐹

Proof of Theorem fvssunirn
StepHypRef Expression
1 fvrn0 6691 . . 3 (𝐹𝑋) ∈ (ran 𝐹 ∪ {∅})
2 elssuni 4859 . . 3 ((𝐹𝑋) ∈ (ran 𝐹 ∪ {∅}) → (𝐹𝑋) ⊆ (ran 𝐹 ∪ {∅}))
31, 2ax-mp 5 . 2 (𝐹𝑋) ⊆ (ran 𝐹 ∪ {∅})
4 uniun 4849 . . 3 (ran 𝐹 ∪ {∅}) = ( ran 𝐹 {∅})
5 0ex 5202 . . . . 5 ∅ ∈ V
65unisn 4846 . . . 4 {∅} = ∅
76uneq2i 4133 . . 3 ( ran 𝐹 {∅}) = ( ran 𝐹 ∪ ∅)
8 un0 4341 . . 3 ( ran 𝐹 ∪ ∅) = ran 𝐹
94, 7, 83eqtri 2845 . 2 (ran 𝐹 ∪ {∅}) = ran 𝐹
103, 9sseqtri 4000 1 (𝐹𝑋) ⊆ ran 𝐹
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  cun 3931  wss 3933  c0 4288  {csn 4557   cuni 4830  ran crn 5549  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-cnv 5556  df-dm 5558  df-rn 5559  df-iota 6307  df-fv 6356
This theorem is referenced by:  ovssunirn  7181  marypha2lem1  8887  acnlem  9462  fin23lem29  9751  itunitc  9831  hsmexlem5  9840  wunfv  10142  wunex2  10148  strfvss  16494  prdsval  16716  prdsbas  16718  prdsplusg  16719  prdsmulr  16720  prdsvsca  16721  prdshom  16728  mreunirn  16860  mrcfval  16867  mrcssv  16873  mrisval  16889  sscpwex  17073  wunfunc  17157  catcxpccl  17445  comppfsc  22068  filunirn  22418  elflim  22507  flffval  22525  fclsval  22544  isfcls  22545  fcfval  22569  tsmsxplem1  22688  xmetunirn  22874  mopnval  22975  tmsval  23018  cfilfval  23794  caufval  23805  issgon  31281  elrnsiga  31284  volmeas  31389  omssubadd  31457  neibastop2lem  33605  ctbssinf  34569  ismtyval  34959  dicval  38192  ismrc  39176  nacsfix  39187  hbt  39608
  Copyright terms: Public domain W3C validator