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

Theorem funiunfv 6986
 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 𝐹 Fn 𝐴, 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 𝐹 𝑥𝐴 (𝐹𝑥) = (𝐹𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Proof of Theorem funiunfv
StepHypRef Expression
1 funres 6367 . . . 4 (Fun 𝐹 → Fun (𝐹𝐴))
21funfnd 6356 . . 3 (Fun 𝐹 → (𝐹𝐴) Fn dom (𝐹𝐴))
3 fniunfv 6985 . . 3 ((𝐹𝐴) Fn dom (𝐹𝐴) → 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) = ran (𝐹𝐴))
42, 3syl 17 . 2 (Fun 𝐹 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) = ran (𝐹𝐴))
5 undif2 4383 . . . . 5 (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴))) = (dom (𝐹𝐴) ∪ 𝐴)
6 dmres 5841 . . . . . . 7 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
7 inss1 4155 . . . . . . 7 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
86, 7eqsstri 3949 . . . . . 6 dom (𝐹𝐴) ⊆ 𝐴
9 ssequn1 4107 . . . . . 6 (dom (𝐹𝐴) ⊆ 𝐴 ↔ (dom (𝐹𝐴) ∪ 𝐴) = 𝐴)
108, 9mpbi 233 . . . . 5 (dom (𝐹𝐴) ∪ 𝐴) = 𝐴
115, 10eqtri 2821 . . . 4 (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴))) = 𝐴
12 iuneq1 4898 . . . 4 ((dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴))) = 𝐴 𝑥 ∈ (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴)))((𝐹𝐴)‘𝑥) = 𝑥𝐴 ((𝐹𝐴)‘𝑥))
1311, 12ax-mp 5 . . 3 𝑥 ∈ (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴)))((𝐹𝐴)‘𝑥) = 𝑥𝐴 ((𝐹𝐴)‘𝑥)
14 iunxun 4980 . . . 4 𝑥 ∈ (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴)))((𝐹𝐴)‘𝑥) = ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥))
15 eldifn 4055 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴)) → ¬ 𝑥 ∈ dom (𝐹𝐴))
16 ndmfv 6676 . . . . . . . . 9 𝑥 ∈ dom (𝐹𝐴) → ((𝐹𝐴)‘𝑥) = ∅)
1715, 16syl 17 . . . . . . . 8 (𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴)) → ((𝐹𝐴)‘𝑥) = ∅)
1817iuneq2i 4903 . . . . . . 7 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥) = 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))∅
19 iun0 4949 . . . . . . 7 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))∅ = ∅
2018, 19eqtri 2821 . . . . . 6 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥) = ∅
2120uneq2i 4087 . . . . 5 ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥)) = ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ ∅)
22 un0 4298 . . . . 5 ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ ∅) = 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥)
2321, 22eqtri 2821 . . . 4 ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥)) = 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥)
2414, 23eqtri 2821 . . 3 𝑥 ∈ (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴)))((𝐹𝐴)‘𝑥) = 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥)
25 fvres 6665 . . . 4 (𝑥𝐴 → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
2625iuneq2i 4903 . . 3 𝑥𝐴 ((𝐹𝐴)‘𝑥) = 𝑥𝐴 (𝐹𝑥)
2713, 24, 263eqtr3ri 2830 . 2 𝑥𝐴 (𝐹𝑥) = 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥)
28 df-ima 5533 . . 3 (𝐹𝐴) = ran (𝐹𝐴)
2928unieqi 4814 . 2 (𝐹𝐴) = ran (𝐹𝐴)
304, 27, 293eqtr4g 2858 1 (Fun 𝐹 𝑥𝐴 (𝐹𝑥) = (𝐹𝐴))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ∈ wcel 2111   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ∪ cuni 4801  ∪ ciun 4882  dom cdm 5520  ran crn 5521   ↾ cres 5522   “ cima 5523  Fun wfun 6319   Fn wfn 6320  ‘cfv 6325 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5426  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-iota 6284  df-fun 6327  df-fn 6328  df-fv 6333 This theorem is referenced by:  funiunfvf  6987  eluniima  6988  marypha2lem4  8889  r1limg  9187  r1elssi  9221  r1elss  9222  ackbij2  9657  r1om  9658  ttukeylem6  9928  isacs2  16919  mreacs  16924  acsfn  16925  isacs5  17777  dprdss  19148  dprd2dlem1  19160  dmdprdsplit2lem  19164  uniioombllem3a  24198  uniioombllem4  24200  uniioombllem5  24201  dyadmbl  24214  mblfinlem1  35113  ovoliunnfl  35118  voliunnfl  35120  uniimafveqt  43941  imasetpreimafvbijlemfv  43962
 Copyright terms: Public domain W3C validator