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

Theorem funiunfv 6061
Description: The indexed union of a function's values is the union of its image under the index class.

Note: This theorem depends on the fact that our function value is the empty set outside of its domain. If the antecedent is changed to  F  Fn  A, the theorem can be proved without this dependency. (Contributed by NM, 26-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)

Assertion
Ref Expression
funiunfv  |-  ( Fun 
F  ->  U_ x  e.  A  ( F `  x )  =  U. ( F " A ) )
Distinct variable groups:    x, A    x, F

Proof of Theorem funiunfv
StepHypRef Expression
1 funres 5535 . . . 4  |-  ( Fun 
F  ->  Fun  ( F  |`  A ) )
2 funfn 5525 . . . 4  |-  ( Fun  ( F  |`  A )  <-> 
( F  |`  A )  Fn  dom  ( F  |`  A ) )
31, 2sylib 196 . . 3  |-  ( Fun 
F  ->  ( F  |`  A )  Fn  dom  ( F  |`  A ) )
4 fniunfv 6060 . . 3  |-  ( ( F  |`  A )  Fn  dom  ( F  |`  A )  ->  U_ x  e.  dom  ( F  |`  A ) ( ( F  |`  A ) `  x )  =  U. ran  ( F  |`  A ) )
53, 4syl 16 . 2  |-  ( Fun 
F  ->  U_ x  e. 
dom  ( F  |`  A ) ( ( F  |`  A ) `  x )  =  U. ran  ( F  |`  A ) )
6 undif2 3820 . . . . 5  |-  ( dom  ( F  |`  A )  u.  ( A  \  dom  ( F  |`  A ) ) )  =  ( dom  ( F  |`  A )  u.  A
)
7 dmres 5206 . . . . . . 7  |-  dom  ( F  |`  A )  =  ( A  i^i  dom  F )
8 inss1 3632 . . . . . . 7  |-  ( A  i^i  dom  F )  C_  A
97, 8eqsstri 3447 . . . . . 6  |-  dom  ( F  |`  A )  C_  A
10 ssequn1 3588 . . . . . 6  |-  ( dom  ( F  |`  A ) 
C_  A  <->  ( dom  ( F  |`  A )  u.  A )  =  A )
119, 10mpbi 208 . . . . 5  |-  ( dom  ( F  |`  A )  u.  A )  =  A
126, 11eqtri 2411 . . . 4  |-  ( dom  ( F  |`  A )  u.  ( A  \  dom  ( F  |`  A ) ) )  =  A
13 iuneq1 4257 . . . 4  |-  ( ( dom  ( F  |`  A )  u.  ( A  \  dom  ( F  |`  A ) ) )  =  A  ->  U_ x  e.  ( dom  ( F  |`  A )  u.  ( A  \  dom  ( F  |`  A ) ) ) ( ( F  |`  A ) `  x
)  =  U_ x  e.  A  ( ( F  |`  A ) `  x ) )
1412, 13ax-mp 5 . . 3  |-  U_ x  e.  ( dom  ( F  |`  A )  u.  ( A  \  dom  ( F  |`  A ) ) ) ( ( F  |`  A ) `  x
)  =  U_ x  e.  A  ( ( F  |`  A ) `  x )
15 iunxun 4328 . . . 4  |-  U_ x  e.  ( dom  ( F  |`  A )  u.  ( A  \  dom  ( F  |`  A ) ) ) ( ( F  |`  A ) `  x
)  =  ( U_ x  e.  dom  ( F  |`  A ) ( ( F  |`  A ) `  x )  u.  U_ x  e.  ( A  \  dom  ( F  |`  A ) ) ( ( F  |`  A ) `
 x ) )
16 eldifn 3541 . . . . . . . . 9  |-  ( x  e.  ( A  \  dom  ( F  |`  A ) )  ->  -.  x  e.  dom  ( F  |`  A ) )
17 ndmfv 5798 . . . . . . . . 9  |-  ( -.  x  e.  dom  ( F  |`  A )  -> 
( ( F  |`  A ) `  x
)  =  (/) )
1816, 17syl 16 . . . . . . . 8  |-  ( x  e.  ( A  \  dom  ( F  |`  A ) )  ->  ( ( F  |`  A ) `  x )  =  (/) )
1918iuneq2i 4262 . . . . . . 7  |-  U_ x  e.  ( A  \  dom  ( F  |`  A ) ) ( ( F  |`  A ) `  x
)  =  U_ x  e.  ( A  \  dom  ( F  |`  A ) ) (/)
20 iun0 4299 . . . . . . 7  |-  U_ x  e.  ( A  \  dom  ( F  |`  A ) ) (/)  =  (/)
2119, 20eqtri 2411 . . . . . 6  |-  U_ x  e.  ( A  \  dom  ( F  |`  A ) ) ( ( F  |`  A ) `  x
)  =  (/)
2221uneq2i 3569 . . . . 5  |-  ( U_ x  e.  dom  ( F  |`  A ) ( ( F  |`  A ) `  x )  u.  U_ x  e.  ( A  \  dom  ( F  |`  A ) ) ( ( F  |`  A ) `
 x ) )  =  ( U_ x  e.  dom  ( F  |`  A ) ( ( F  |`  A ) `  x )  u.  (/) )
23 un0 3737 . . . . 5  |-  ( U_ x  e.  dom  ( F  |`  A ) ( ( F  |`  A ) `  x )  u.  (/) )  = 
U_ x  e.  dom  ( F  |`  A ) ( ( F  |`  A ) `  x
)
2422, 23eqtri 2411 . . . 4  |-  ( U_ x  e.  dom  ( F  |`  A ) ( ( F  |`  A ) `  x )  u.  U_ x  e.  ( A  \  dom  ( F  |`  A ) ) ( ( F  |`  A ) `
 x ) )  =  U_ x  e. 
dom  ( F  |`  A ) ( ( F  |`  A ) `  x )
2515, 24eqtri 2411 . . 3  |-  U_ x  e.  ( dom  ( F  |`  A )  u.  ( A  \  dom  ( F  |`  A ) ) ) ( ( F  |`  A ) `  x
)  =  U_ x  e.  dom  ( F  |`  A ) ( ( F  |`  A ) `  x )
26 fvres 5788 . . . 4  |-  ( x  e.  A  ->  (
( F  |`  A ) `
 x )  =  ( F `  x
) )
2726iuneq2i 4262 . . 3  |-  U_ x  e.  A  ( ( F  |`  A ) `  x )  =  U_ x  e.  A  ( F `  x )
2814, 25, 273eqtr3ri 2420 . 2  |-  U_ x  e.  A  ( F `  x )  =  U_ x  e.  dom  ( F  |`  A ) ( ( F  |`  A ) `  x )
29 df-ima 4926 . . 3  |-  ( F
" A )  =  ran  ( F  |`  A )
3029unieqi 4172 . 2  |-  U. ( F " A )  = 
U. ran  ( F  |`  A )
315, 28, 303eqtr4g 2448 1  |-  ( Fun 
F  ->  U_ x  e.  A  ( F `  x )  =  U. ( F " A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1399    e. wcel 1826    \ cdif 3386    u. cun 3387    i^i cin 3388    C_ wss 3389   (/)c0 3711   U.cuni 4163   U_ciun 4243   dom cdm 4913   ran crn 4914    |` cres 4915   "cima 4916   Fun wfun 5490    Fn wfn 5491   ` cfv 5496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-fv 5504
This theorem is referenced by:  funiunfvf  6062  eluniima  6063  marypha2lem4  7813  r1limg  8102  r1elssi  8136  r1elss  8137  ackbij2  8536  r1om  8537  ttukeylem6  8807  isacs2  15060  mreacs  15065  acsfn  15066  isacs5  15919  dprdss  17189  dprd2dlem1  17203  dmdprdsplit2lem  17207  uniioombllem3a  22078  uniioombllem4  22080  uniioombllem5  22081  dyadmbl  22094  mblfinlem1  30216  ovoliunnfl  30221  voliunnfl  30223
  Copyright terms: Public domain W3C validator