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

Theorem funiunfv 7243
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 6584 . . . 4 (Fun 𝐹 → Fun (𝐹𝐴))
21funfnd 6573 . . 3 (Fun 𝐹 → (𝐹𝐴) Fn dom (𝐹𝐴))
3 fniunfv 7242 . . 3 ((𝐹𝐴) Fn dom (𝐹𝐴) → 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) = ran (𝐹𝐴))
42, 3syl 17 . 2 (Fun 𝐹 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) = ran (𝐹𝐴))
5 undif2 4471 . . . . 5 (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴))) = (dom (𝐹𝐴) ∪ 𝐴)
6 dmres 5997 . . . . . . 7 dom (𝐹𝐴) = (𝐴 ∩ dom 𝐹)
7 inss1 4223 . . . . . . 7 (𝐴 ∩ dom 𝐹) ⊆ 𝐴
86, 7eqsstri 4011 . . . . . 6 dom (𝐹𝐴) ⊆ 𝐴
9 ssequn1 4175 . . . . . 6 (dom (𝐹𝐴) ⊆ 𝐴 ↔ (dom (𝐹𝐴) ∪ 𝐴) = 𝐴)
108, 9mpbi 229 . . . . 5 (dom (𝐹𝐴) ∪ 𝐴) = 𝐴
115, 10eqtri 2754 . . . 4 (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴))) = 𝐴
12 iuneq1 5006 . . . 4 ((dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴))) = 𝐴 𝑥 ∈ (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴)))((𝐹𝐴)‘𝑥) = 𝑥𝐴 ((𝐹𝐴)‘𝑥))
1311, 12ax-mp 5 . . 3 𝑥 ∈ (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴)))((𝐹𝐴)‘𝑥) = 𝑥𝐴 ((𝐹𝐴)‘𝑥)
14 iunxun 5090 . . . 4 𝑥 ∈ (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴)))((𝐹𝐴)‘𝑥) = ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥))
15 eldifn 4122 . . . . . . . . 9 (𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴)) → ¬ 𝑥 ∈ dom (𝐹𝐴))
16 ndmfv 6920 . . . . . . . . 9 𝑥 ∈ dom (𝐹𝐴) → ((𝐹𝐴)‘𝑥) = ∅)
1715, 16syl 17 . . . . . . . 8 (𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴)) → ((𝐹𝐴)‘𝑥) = ∅)
1817iuneq2i 5011 . . . . . . 7 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥) = 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))∅
19 iun0 5058 . . . . . . 7 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))∅ = ∅
2018, 19eqtri 2754 . . . . . 6 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥) = ∅
2120uneq2i 4155 . . . . 5 ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥)) = ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ ∅)
22 un0 4385 . . . . 5 ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ ∅) = 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥)
2321, 22eqtri 2754 . . . 4 ( 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥) ∪ 𝑥 ∈ (𝐴 ∖ dom (𝐹𝐴))((𝐹𝐴)‘𝑥)) = 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥)
2414, 23eqtri 2754 . . 3 𝑥 ∈ (dom (𝐹𝐴) ∪ (𝐴 ∖ dom (𝐹𝐴)))((𝐹𝐴)‘𝑥) = 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥)
25 fvres 6904 . . . 4 (𝑥𝐴 → ((𝐹𝐴)‘𝑥) = (𝐹𝑥))
2625iuneq2i 5011 . . 3 𝑥𝐴 ((𝐹𝐴)‘𝑥) = 𝑥𝐴 (𝐹𝑥)
2713, 24, 263eqtr3ri 2763 . 2 𝑥𝐴 (𝐹𝑥) = 𝑥 ∈ dom (𝐹𝐴)((𝐹𝐴)‘𝑥)
28 df-ima 5682 . . 3 (𝐹𝐴) = ran (𝐹𝐴)
2928unieqi 4914 . 2 (𝐹𝐴) = ran (𝐹𝐴)
304, 27, 293eqtr4g 2791 1 (Fun 𝐹 𝑥𝐴 (𝐹𝑥) = (𝐹𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1533  wcel 2098  cdif 3940  cun 3941  cin 3942  wss 3943  c0 4317   cuni 4902   ciun 4990  dom cdm 5669  ran crn 5670  cres 5671  cima 5672  Fun wfun 6531   Fn wfn 6532  cfv 6537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-iota 6489  df-fun 6539  df-fn 6540  df-fv 6545
This theorem is referenced by:  funiunfvf  7244  eluniima  7245  marypha2lem4  9435  r1limg  9768  r1elssi  9802  r1elss  9803  ackbij2  10240  r1om  10241  ttukeylem6  10511  isacs2  17606  mreacs  17611  acsfn  17612  isacs5  18513  dprdss  19951  dprd2dlem1  19963  dmdprdsplit2lem  19967  uniioombllem3a  25468  uniioombllem4  25470  uniioombllem5  25471  dyadmbl  25484  oldlim  27768  precsexlem10  28069  precsexlem11  28070  mblfinlem1  37038  ovoliunnfl  37043  voliunnfl  37045  uniimafveqt  46621  imasetpreimafvbijlemfv  46642
  Copyright terms: Public domain W3C validator