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

Theorem fvun1 6933
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 6603 . . . 4 (𝐹 Fn 𝐴 → Fun 𝐹)
213ad2ant1 1134 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → Fun 𝐹)
3 fnfun 6603 . . . 4 (𝐺 Fn 𝐵 → Fun 𝐺)
433ad2ant2 1135 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → Fun 𝐺)
5 fndm 6606 . . . . . . . 8 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
6 fndm 6606 . . . . . . . 8 (𝐺 Fn 𝐵 → dom 𝐺 = 𝐵)
75, 6ineqan12d 4175 . . . . . . 7 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → (dom 𝐹 ∩ dom 𝐺) = (𝐴𝐵))
87eqeq1d 2739 . . . . . 6 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ (𝐴𝐵) = ∅))
98biimprd 248 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → ((𝐴𝐵) = ∅ → (dom 𝐹 ∩ dom 𝐺) = ∅))
109adantrd 493 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → (((𝐴𝐵) = ∅ ∧ 𝑋𝐴) → (dom 𝐹 ∩ dom 𝐺) = ∅))
11103impia 1118 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → (dom 𝐹 ∩ dom 𝐺) = ∅)
12 fvun 6932 . . 3 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((𝐹𝐺)‘𝑋) = ((𝐹𝑋) ∪ (𝐺𝑋)))
132, 4, 11, 12syl21anc 837 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ((𝐹𝐺)‘𝑋) = ((𝐹𝑋) ∪ (𝐺𝑋)))
14 disjel 4417 . . . . . . . 8 (((𝐴𝐵) = ∅ ∧ 𝑋𝐴) → ¬ 𝑋𝐵)
1514adantl 483 . . . . . . 7 ((𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ¬ 𝑋𝐵)
166eleq2d 2824 . . . . . . . 8 (𝐺 Fn 𝐵 → (𝑋 ∈ dom 𝐺𝑋𝐵))
1716adantr 482 . . . . . . 7 ((𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → (𝑋 ∈ dom 𝐺𝑋𝐵))
1815, 17mtbird 325 . . . . . 6 ((𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ¬ 𝑋 ∈ dom 𝐺)
19183adant1 1131 . . . . 5 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ¬ 𝑋 ∈ dom 𝐺)
20 ndmfv 6878 . . . . 5 𝑋 ∈ dom 𝐺 → (𝐺𝑋) = ∅)
2119, 20syl 17 . . . 4 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → (𝐺𝑋) = ∅)
2221uneq2d 4124 . . 3 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ((𝐹𝑋) ∪ (𝐺𝑋)) = ((𝐹𝑋) ∪ ∅))
23 un0 4351 . . 3 ((𝐹𝑋) ∪ ∅) = (𝐹𝑋)
2422, 23eqtrdi 2793 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ((𝐹𝑋) ∪ (𝐺𝑋)) = (𝐹𝑋))
2513, 24eqtrd 2777 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐵 ∧ ((𝐴𝐵) = ∅ ∧ 𝑋𝐴)) → ((𝐹𝐺)‘𝑋) = (𝐹𝑋))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  cun 3909  cin 3910  c0 4283  dom cdm 5634  Fun wfun 6491   Fn wfn 6492  cfv 6497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-fv 6505
This theorem is referenced by:  fvun2  6934  fvun1d  6935  frrlem12  8229  enfixsn  9026  ptunhmeo  23162  noextenddif  27019  axlowdimlem6  27899  axlowdimlem8  27901  axlowdimlem11  27904  vtxdun  28432  isoun  31618  cycpmfv3  31967  lbsdiflsp0  32324  sseqfv1  32992  reprsuc  33231  breprexplema  33246  cvmliftlem5  33886  fullfunfv  34535  finixpnum  36066  poimirlem1  36082  poimirlem2  36083  poimirlem3  36084  poimirlem4  36085  poimirlem6  36087  poimirlem7  36088  poimirlem11  36092  poimirlem12  36093  poimirlem16  36097  poimirlem17  36098  poimirlem19  36100  poimirlem22  36103  poimirlem23  36104  poimirlem28  36109  aacllem  47255
  Copyright terms: Public domain W3C validator