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

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

Proof of Theorem fun
StepHypRef Expression
1 fnun 6434 . . . . 5 (((𝐹 Fn 𝐴𝐺 Fn 𝐵) ∧ (𝐴𝐵) = ∅) → (𝐹𝐺) Fn (𝐴𝐵))
21expcom 417 . . . 4 ((𝐴𝐵) = ∅ → ((𝐹 Fn 𝐴𝐺 Fn 𝐵) → (𝐹𝐺) Fn (𝐴𝐵)))
3 rnun 5971 . . . . 5 ran (𝐹𝐺) = (ran 𝐹 ∪ ran 𝐺)
4 unss12 4109 . . . . 5 ((ran 𝐹𝐶 ∧ ran 𝐺𝐷) → (ran 𝐹 ∪ ran 𝐺) ⊆ (𝐶𝐷))
53, 4eqsstrid 3963 . . . 4 ((ran 𝐹𝐶 ∧ ran 𝐺𝐷) → ran (𝐹𝐺) ⊆ (𝐶𝐷))
62, 5anim12d1 612 . . 3 ((𝐴𝐵) = ∅ → (((𝐹 Fn 𝐴𝐺 Fn 𝐵) ∧ (ran 𝐹𝐶 ∧ ran 𝐺𝐷)) → ((𝐹𝐺) Fn (𝐴𝐵) ∧ ran (𝐹𝐺) ⊆ (𝐶𝐷))))
7 df-f 6328 . . . . 5 (𝐹:𝐴𝐶 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐶))
8 df-f 6328 . . . . 5 (𝐺:𝐵𝐷 ↔ (𝐺 Fn 𝐵 ∧ ran 𝐺𝐷))
97, 8anbi12i 629 . . . 4 ((𝐹:𝐴𝐶𝐺:𝐵𝐷) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ∧ (𝐺 Fn 𝐵 ∧ ran 𝐺𝐷)))
10 an4 655 . . . 4 (((𝐹 Fn 𝐴 ∧ ran 𝐹𝐶) ∧ (𝐺 Fn 𝐵 ∧ ran 𝐺𝐷)) ↔ ((𝐹 Fn 𝐴𝐺 Fn 𝐵) ∧ (ran 𝐹𝐶 ∧ ran 𝐺𝐷)))
119, 10bitri 278 . . 3 ((𝐹:𝐴𝐶𝐺:𝐵𝐷) ↔ ((𝐹 Fn 𝐴𝐺 Fn 𝐵) ∧ (ran 𝐹𝐶 ∧ ran 𝐺𝐷)))
12 df-f 6328 . . 3 ((𝐹𝐺):(𝐴𝐵)⟶(𝐶𝐷) ↔ ((𝐹𝐺) Fn (𝐴𝐵) ∧ ran (𝐹𝐺) ⊆ (𝐶𝐷)))
136, 11, 123imtr4g 299 . 2 ((𝐴𝐵) = ∅ → ((𝐹:𝐴𝐶𝐺:𝐵𝐷) → (𝐹𝐺):(𝐴𝐵)⟶(𝐶𝐷)))
1413impcom 411 1 (((𝐹:𝐴𝐶𝐺:𝐵𝐷) ∧ (𝐴𝐵) = ∅) → (𝐹𝐺):(𝐴𝐵)⟶(𝐶𝐷))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  ran crn 5520   Fn wfn 6319  ⟶wf 6320 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-id 5425  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-fun 6326  df-fn 6327  df-f 6328 This theorem is referenced by:  fun2  6515  ftpg  6895  fsnunf  6924  ralxpmap  8445  hashfxnn0  13695  cats1un  14076  pwssplit1  19827  axlowdimlem10  26752  wlkp1  27478  padct  30488  eulerpartlemt  31751  sseqf  31772  poimirlem3  35076  poimirlem16  35089  poimirlem19  35092  poimirlem22  35095  poimirlem23  35096  poimirlem24  35097  poimirlem25  35098  poimirlem28  35101  poimirlem29  35102  poimirlem31  35104  mapfzcons  39672  diophrw  39715  diophren  39769  pwssplit4  40048  aacllem  45343
 Copyright terms: Public domain W3C validator