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

Theorem fvun1 6925
Description: The value of a union when the argument is in the first domain. (Contributed by Scott Fenton, 29-Jun-2013.)
Assertion
Ref Expression
fvun1 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ((𝐹𝐺)‘𝑋) = (𝐹𝑋))

Proof of Theorem fvun1
StepHypRef Expression
1 fnfun 6592 . . . 4 (𝐹 Fn 𝐴 → Fun 𝐹)
213ad2ant1 1133 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → Fun 𝐹)
3 fnfun 6592 . . . 4 (𝐺 Fn 𝐵 → Fun 𝐺)
433ad2ant2 1134 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → Fun 𝐺)
5 fndm 6595 . . . . . . . 8 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
6 fndm 6595 . . . . . . . 8 (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
75, 6ineqan12d 4174 . . . . . . 7 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → (dom 𝐹 ∩ dom 𝐺) = (𝐴𝐵))
87eqeq1d 2738 . . . . . 6 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ (𝐴𝐵) = ∅))
98biimprd 248 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → ((𝐴𝐵) = ∅ → (dom 𝐹 ∩ dom 𝐺) = ∅))
109adantrd 491 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → (((𝐴𝐵) = ∅ ∧ 𝑋𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅))
11103impia 1117 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
12 fvun 6924 . . 3 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹𝐺)‘𝑋) = ((𝐹𝑋) ∪ (𝐺𝑋)))
132, 4, 11, 12syl21anc 837 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ((𝐹𝐺)‘𝑋) = ((𝐹𝑋) ∪ (𝐺𝑋)))
14 disjel 4409 . . . . . . . 8 (((𝐴𝐵) = ∅ ∧ 𝑋𝐴) → ¬ 𝑋𝐵)
1514adantl 481 . . . . . . 7 ((𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ¬ 𝑋𝐵)
166eleq2d 2822 . . . . . . . 8 (𝐺 Fn 𝐵 → (𝑋 ∈ dom 𝐺𝑋𝐵))
1716adantr 480 . . . . . . 7 ((𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → (𝑋 ∈ dom 𝐺𝑋𝐵))
1815, 17mtbird 325 . . . . . 6 ((𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ¬ 𝑋 ∈ dom 𝐺)
19183adant1 1130 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ¬ 𝑋 ∈ dom 𝐺)
20 ndmfv 6866 . . . . 5 𝑋 ∈ dom 𝐺 → (𝐺𝑋) = ∅)
2119, 20syl 17 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → (𝐺𝑋) = ∅)
2221uneq2d 4120 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ((𝐹𝑋) ∪ (𝐺𝑋)) = ((𝐹𝑋) ∪ ∅))
23 un0 4346 . . 3 ((𝐹𝑋) ∪ ∅) = (𝐹𝑋)
2422, 23eqtrdi 2787 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ((𝐹𝑋) ∪ (𝐺𝑋)) = (𝐹𝑋))
2513, 24eqtrd 2771 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ((𝐹𝐺)‘𝑋) = (𝐹𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1541  wcel 2113  cun 3899  cin 3900  c0 4285  dom cdm 5624  Fun wfun 6486   Fn wfn 6487  cfv 6492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500
This theorem is referenced by:  fvun2  6926  fvun1d  6927  frrlem12  8239  enfixsn  9014  ptunhmeo  23752  noextenddif  27636  axlowdimlem6  29020  axlowdimlem8  29022  axlowdimlem11  29025  vtxdun  29555  isoun  32781  cycpmfv3  33197  lbsdiflsp0  33783  sseqfv1  34546  reprsuc  34772  breprexplema  34787  cvmliftlem5  35483  fullfunfv  36141  finixpnum  37802  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem4  37821  poimirlem6  37823  poimirlem7  37824  poimirlem11  37828  poimirlem12  37829  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem22  37839  poimirlem23  37840  poimirlem28  37845  aacllem  50042
  Copyright terms: Public domain W3C validator