![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > funiunfv | Unicode version |
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 , the theorem can be proved without this dependency. (Contributed by NM, 26-Mar-2006.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
funiunfv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | funres 5632 | . . . 4 | |
2 | funfn 5622 | . . . 4 | |
3 | 1, 2 | sylib 196 | . . 3 |
4 | fniunfv 6159 | . . 3 | |
5 | 3, 4 | syl 16 | . 2 |
6 | undif2 3904 | . . . . 5 | |
7 | dmres 5299 | . . . . . . 7 | |
8 | inss1 3717 | . . . . . . 7 | |
9 | 7, 8 | eqsstri 3533 | . . . . . 6 |
10 | ssequn1 3673 | . . . . . 6 | |
11 | 9, 10 | mpbi 208 | . . . . 5 |
12 | 6, 11 | eqtri 2486 | . . . 4 |
13 | iuneq1 4344 | . . . 4 | |
14 | 12, 13 | ax-mp 5 | . . 3 |
15 | iunxun 4412 | . . . 4 | |
16 | eldifn 3626 | . . . . . . . . 9 | |
17 | ndmfv 5895 | . . . . . . . . 9 | |
18 | 16, 17 | syl 16 | . . . . . . . 8 |
19 | 18 | iuneq2i 4349 | . . . . . . 7 |
20 | iun0 4386 | . . . . . . 7 | |
21 | 19, 20 | eqtri 2486 | . . . . . 6 |
22 | 21 | uneq2i 3654 | . . . . 5 |
23 | un0 3810 | . . . . 5 | |
24 | 22, 23 | eqtri 2486 | . . . 4 |
25 | 15, 24 | eqtri 2486 | . . 3 |
26 | fvres 5885 | . . . 4 | |
27 | 26 | iuneq2i 4349 | . . 3 |
28 | 14, 25, 27 | 3eqtr3ri 2495 | . 2 |
29 | df-ima 5017 | . . 3 | |
30 | 29 | unieqi 4258 | . 2 |
31 | 5, 28, 30 | 3eqtr4g 2523 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -. wn 3 -> wi 4
= wceq 1395 e. wcel 1818 \ cdif 3472
u. cun 3473 i^i cin 3474 C_ wss 3475
c0 3784 U. cuni 4249 U_ ciun 4330
dom cdm 5004 ran crn 5005 |` cres 5006
" cima 5007 Fun wfun 5587 Fn wfn 5588
` cfv 5593 |
This theorem is referenced by: funiunfvf 6161 eluniima 6162 marypha2lem4 7918 r1limg 8210 r1elssi 8244 r1elss 8245 ackbij2 8644 r1om 8645 ttukeylem6 8915 isacs2 15050 mreacs 15055 acsfn 15056 isacs5 15802 dprdss 17076 dprd2dlem1 17090 dmdprdsplit2lem 17094 uniioombllem3a 21993 uniioombllem4 21995 uniioombllem5 21996 dyadmbl 22009 mblfinlem1 30051 ovoliunnfl 30056 voliunnfl 30058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1618 ax-4 1631 ax-5 1704 ax-6 1747 ax-7 1790 ax-8 1820 ax-9 1822 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 ax-sep 4573 ax-nul 4581 ax-pow 4630 ax-pr 4691 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1398 df-ex 1613 df-nf 1617 df-sb 1740 df-eu 2286 df-mo 2287 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 df-sbc 3328 df-dif 3478 df-un 3480 df-in 3482 df-ss 3489 df-nul 3785 df-if 3942 df-sn 4030 df-pr 4032 df-op 4036 df-uni 4250 df-iun 4332 df-br 4453 df-opab 4511 df-mpt 4512 df-id 4800 df-xp 5010 df-rel 5011 df-cnv 5012 df-co 5013 df-dm 5014 df-rn 5015 df-res 5016 df-ima 5017 df-iota 5556 df-fun 5595 df-fn 5596 df-fv 5601 |
Copyright terms: Public domain | W3C validator |