Theorem fun 6689

Description: The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004.)

Assertion

Ref	Expression
fun	⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷))

Proof of Theorem fun

Step	Hyp	Ref	Expression
1		fnun 6599	. . . . 5 ⊢ (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵))
2	1	expcom 414	. . . 4 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) → (𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵)))
3		rnun 6096	. . . . 5 ⊢ ran (𝐹 ∪ 𝐺) = (ran 𝐹 ∪ ran 𝐺)
4		unss12 4117	. . . . 5 ⊢ ((ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷) → (ran 𝐹 ∪ ran 𝐺) ⊆ (𝐶 ∪ 𝐷))
5	3, 4	eqsstrid 3953	. . . 4 ⊢ ((ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷) → ran (𝐹 ∪ 𝐺) ⊆ (𝐶 ∪ 𝐷))
6	2, 5	anim12d1 616	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ → (((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷)) → ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵) ∧ ran (𝐹 ∪ 𝐺) ⊆ (𝐶 ∪ 𝐷))))
7		df-f 6489	. . . . 5 ⊢ (𝐹:𝐴⟶𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶))
8		df-f 6489	. . . . 5 ⊢ (𝐺:𝐵⟶𝐷 ↔ (𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷))
9	7, 8	anbi12i 634	. . . 4 ⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷)))
10		an4 662	. . . 4 ⊢ (((𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶) ∧ (𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐷)) ↔ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷)))
11	9, 10	bitri 276	. . 3 ⊢ ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ↔ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵) ∧ (ran 𝐹 ⊆ 𝐶 ∧ ran 𝐺 ⊆ 𝐷)))
12		df-f 6489	. . 3 ⊢ ((𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷) ↔ ((𝐹 ∪ 𝐺) Fn (𝐴 ∪ 𝐵) ∧ ran (𝐹 ∪ 𝐺) ⊆ (𝐶 ∪ 𝐷)))
13	6, 11, 12	3imtr4g 297	. 2 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷)))
14	13	impcom 408	1 ⊢ (((𝐹:𝐴⟶𝐶 ∧ 𝐺:𝐵⟶𝐷) ∧ (𝐴 ∩ 𝐵) = ∅) → (𝐹 ∪ 𝐺):(𝐴 ∪ 𝐵)⟶(𝐶 ∪ 𝐷))

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4261  ran crn 5619   Fn wfn 6480  ⟶wf 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-fun 6487  df-fn 6488  df-f 6489

This theorem is referenced by:  fun2  6690  ftpg  7099  fsnunf  7129  ralxpmap  8834  hashfxnn0  14290  cats1un  14674  pwssplit1  21049  axlowdimlem10  29038  wlkp1  29766  padct  32810  eulerpartlemt  34555  sseqf  34576  poimirlem3  37990  poimirlem16  38003  poimirlem19  38006  poimirlem22  38009  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem28  38015  poimirlem29  38016  poimirlem31  38018  mapfzcons  43165  diophrw  43208  diophren  43258  pwssplit4  43534  aacllem  50291