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

Theorem fnun 6035
Description: The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)
Assertion
Ref Expression
fnun (((𝐹 Fn 𝐴𝐺 Fn 𝐵) ∧ (𝐴𝐵) = ∅) → (𝐹𝐺) Fn (𝐴𝐵))

Proof of Theorem fnun
StepHypRef Expression
1 df-fn 5929 . . 3 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2 df-fn 5929 . . 3 (𝐺 Fn 𝐵 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐵))
3 ineq12 3842 . . . . . . . . . . 11 ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (dom 𝐹 ∩ dom 𝐺) = (𝐴𝐵))
43eqeq1d 2653 . . . . . . . . . 10 ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ (𝐴𝐵) = ∅))
54anbi2d 740 . . . . . . . . 9 ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) ↔ ((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴𝐵) = ∅)))
6 funun 5970 . . . . . . . . 9 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹𝐺))
75, 6syl6bir 244 . . . . . . . 8 ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴𝐵) = ∅) → Fun (𝐹𝐺)))
8 dmun 5363 . . . . . . . . 9 dom (𝐹𝐺) = (dom 𝐹 ∪ dom 𝐺)
9 uneq12 3795 . . . . . . . . 9 ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (dom 𝐹 ∪ dom 𝐺) = (𝐴𝐵))
108, 9syl5eq 2697 . . . . . . . 8 ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → dom (𝐹𝐺) = (𝐴𝐵))
117, 10jctird 566 . . . . . . 7 ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴𝐵) = ∅) → (Fun (𝐹𝐺) ∧ dom (𝐹𝐺) = (𝐴𝐵))))
12 df-fn 5929 . . . . . . 7 ((𝐹𝐺) Fn (𝐴𝐵) ↔ (Fun (𝐹𝐺) ∧ dom (𝐹𝐺) = (𝐴𝐵)))
1311, 12syl6ibr 242 . . . . . 6 ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴𝐵) = ∅) → (𝐹𝐺) Fn (𝐴𝐵)))
1413expd 451 . . . . 5 ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → ((Fun 𝐹 ∧ Fun 𝐺) → ((𝐴𝐵) = ∅ → (𝐹𝐺) Fn (𝐴𝐵))))
1514impcom 445 . . . 4 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵)) → ((𝐴𝐵) = ∅ → (𝐹𝐺) Fn (𝐴𝐵)))
1615an4s 886 . . 3 (((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ∧ (Fun 𝐺 ∧ dom 𝐺 = 𝐵)) → ((𝐴𝐵) = ∅ → (𝐹𝐺) Fn (𝐴𝐵)))
171, 2, 16syl2anb 495 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → ((𝐴𝐵) = ∅ → (𝐹𝐺) Fn (𝐴𝐵)))
1817imp 444 1 (((𝐹 Fn 𝐴𝐺 Fn 𝐵) ∧ (𝐴𝐵) = ∅) → (𝐹𝐺) Fn (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383   = wceq 1523  cun 3605  cin 3606  c0 3948  dom cdm 5143  Fun wfun 5920   Fn wfn 5921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-id 5053  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-fun 5928  df-fn 5929
This theorem is referenced by:  fnunsn  6036  fun  6104  foun  6193  f1oun  6194  undifixp  7986  brwdom2  8519  sseqfn  30580  bnj927  30965  bnj535  31086  fullfunfnv  32178  finixpnum  33524  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559
  Copyright terms: Public domain W3C validator