Theorem fnun 6656

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

Step	Hyp	Ref	Expression
1		df-fn 6544	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2		df-fn 6544	. . 3 ⊢ (𝐺 Fn 𝐵 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐵))
3		ineq12 4111	. . . . . . . . . . 11 ⊢ ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (dom 𝐹 ∩ dom 𝐺) = (𝐴 ∩ 𝐵))
4	3	eqeq1d 2762	. . . . . . . . . 10 ⊢ ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ (𝐴 ∩ 𝐵) = ∅))
5	4	anbi2d 642	. . . . . . . . 9 ⊢ ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) ↔ ((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴 ∩ 𝐵) = ∅)))
6		funun 6589	. . . . . . . . 9 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺))
7	5, 6	biimtrrdi 257	. . . . . . . 8 ⊢ ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴 ∩ 𝐵) = ∅) → Fun (𝐹 ∪ 𝐺)))
8		dmun 5892	. . . . . . . . 9 ⊢ dom (𝐹 ∪ 𝐺) = (dom 𝐹 ∪ dom 𝐺)
9		uneq12 4161	. . . . . . . . 9 ⊢ ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (dom 𝐹 ∪ dom 𝐺) = (𝐴 ∪ 𝐵))
10	8, 9	eqtrid 2807	. . . . . . . 8 ⊢ ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → dom (𝐹 ∪ 𝐺) = (𝐴 ∪ 𝐵))
11	7, 10	jctird 536	. . . . . . 7 ⊢ ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴 ∩ 𝐵) = ∅) → (Fun (𝐹 ∪ 𝐺) ∧ dom (𝐹 ∪ 𝐺) = (𝐴 ∪ 𝐵))))
12		df-fn 6544	. . . . . . 7 ⊢ ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵) ↔ (Fun (𝐹 ∪ 𝐺) ∧ dom (𝐹 ∪ 𝐺) = (𝐴 ∪ 𝐵)))
13	11, 12	imbitrrdi 255	. . . . . 6 ⊢ ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → (((Fun 𝐹 ∧ Fun 𝐺) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)))
14	13	expd 421	. . . . 5 ⊢ ((dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵) → ((Fun 𝐹 ∧ Fun 𝐺) → ((𝐴 ∩ 𝐵) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))))
15	14	impcom 413	. . . 4 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 = 𝐴 ∧ dom 𝐺 = 𝐵)) → ((𝐴 ∩ 𝐵) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)))
16	15	an4s 673	. . 3 ⊢ (((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ∧ (Fun 𝐺 ∧ dom 𝐺 = 𝐵)) → ((𝐴 ∩ 𝐵) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)))
17	1, 2, 16	syl2anb 610	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → ((𝐴 ∩ 𝐵) = ∅ → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)))
18	17	imp 412	1 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∩ cin 4088   ∪ cun 4148  ∅c0 4277  dom cdm 5650  Fun wfun 6535   Fn wfn 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-fun 6543  df-fn 6544

This theorem is used by:  fnund  6657  fun  6747  foun  6846  f1oun  6847  frrlem11  8319  undifixp  8967  bnj535  35568  fullfunfnv  36804  finixpnum  38635  poimirlem1  38646  poimirlem2  38647  poimirlem3  38648  poimirlem4  38649  poimirlem6  38651  poimirlem7  38652  poimirlem11  38656  poimirlem12  38657  poimirlem16  38661  poimirlem17  38662  poimirlem19  38664  poimirlem20  38665