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

Theorem funun 5846
 Description: The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43. (Contributed by NM, 12-Aug-1994.)
Assertion
Ref Expression
funun (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹𝐺))

Proof of Theorem funun
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funrel 5821 . . . . 5 (Fun 𝐹 → Rel 𝐹)
2 funrel 5821 . . . . 5 (Fun 𝐺 → Rel 𝐺)
31, 2anim12i 588 . . . 4 ((Fun 𝐹 ∧ Fun 𝐺) → (Rel 𝐹 ∧ Rel 𝐺))
4 relun 5158 . . . 4 (Rel (𝐹𝐺) ↔ (Rel 𝐹 ∧ Rel 𝐺))
53, 4sylibr 223 . . 3 ((Fun 𝐹 ∧ Fun 𝐺) → Rel (𝐹𝐺))
65adantr 480 . 2 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Rel (𝐹𝐺))
7 elun 3715 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
8 elun 3715 . . . . . . . 8 (⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
97, 8anbi12i 729 . . . . . . 7 ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
10 anddi 910 . . . . . . 7 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
119, 10bitri 263 . . . . . 6 ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
12 disj1 3971 . . . . . . . . . . . . 13 ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
1312biimpi 205 . . . . . . . . . . . 12 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
141319.21bi 2047 . . . . . . . . . . 11 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
15 imnan 437 . . . . . . . . . . 11 ((𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺) ↔ ¬ (𝑥 ∈ dom 𝐹𝑥 ∈ dom 𝐺))
1614, 15sylib 207 . . . . . . . . . 10 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐹𝑥 ∈ dom 𝐺))
17 vex 3176 . . . . . . . . . . . 12 𝑥 ∈ V
18 vex 3176 . . . . . . . . . . . 12 𝑦 ∈ V
1917, 18opeldm 5250 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐹𝑥 ∈ dom 𝐹)
20 vex 3176 . . . . . . . . . . . 12 𝑧 ∈ V
2117, 20opeldm 5250 . . . . . . . . . . 11 (⟨𝑥, 𝑧⟩ ∈ 𝐺𝑥 ∈ dom 𝐺)
2219, 21anim12i 588 . . . . . . . . . 10 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (𝑥 ∈ dom 𝐹𝑥 ∈ dom 𝐺))
2316, 22nsyl 134 . . . . . . . . 9 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
24 orel2 397 . . . . . . . . 9 (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
2523, 24syl 17 . . . . . . . 8 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
2614con2d 128 . . . . . . . . . . 11 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹))
27 imnan 437 . . . . . . . . . . 11 ((𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹) ↔ ¬ (𝑥 ∈ dom 𝐺𝑥 ∈ dom 𝐹))
2826, 27sylib 207 . . . . . . . . . 10 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐺𝑥 ∈ dom 𝐹))
2917, 18opeldm 5250 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐺𝑥 ∈ dom 𝐺)
3017, 20opeldm 5250 . . . . . . . . . . 11 (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥 ∈ dom 𝐹)
3129, 30anim12i 588 . . . . . . . . . 10 ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑥 ∈ dom 𝐺𝑥 ∈ dom 𝐹))
3228, 31nsyl 134 . . . . . . . . 9 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
33 orel1 396 . . . . . . . . 9 (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
3432, 33syl 17 . . . . . . . 8 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
3525, 34orim12d 879 . . . . . . 7 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
3635adantl 481 . . . . . 6 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
3711, 36syl5bi 231 . . . . 5 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
38 dffun4 5816 . . . . . . . . . 10 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
3938simprbi 479 . . . . . . . . 9 (Fun 𝐹 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
403919.21bi 2047 . . . . . . . 8 (Fun 𝐹 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
414019.21bbi 2048 . . . . . . 7 (Fun 𝐹 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
42 dffun4 5816 . . . . . . . . . 10 (Fun 𝐺 ↔ (Rel 𝐺 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧)))
4342simprbi 479 . . . . . . . . 9 (Fun 𝐺 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
444319.21bi 2047 . . . . . . . 8 (Fun 𝐺 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
454419.21bbi 2048 . . . . . . 7 (Fun 𝐺 → ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
4641, 45jaao 530 . . . . . 6 ((Fun 𝐹 ∧ Fun 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
4746adantr 480 . . . . 5 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
4837, 47syld 46 . . . 4 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧))
4948alrimiv 1842 . . 3 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧))
5049alrimivv 1843 . 2 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧))
51 dffun4 5816 . 2 (Fun (𝐹𝐺) ↔ (Rel (𝐹𝐺) ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧)))
526, 50, 51sylanbrc 695 1 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹𝐺))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 382   ∧ wa 383  ∀wal 1473   = wceq 1475   ∈ wcel 1977   ∪ cun 3538   ∩ cin 3539  ∅c0 3874  ⟨cop 4131  dom cdm 5038  Rel wrel 5043  Fun wfun 5798 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-id 4953  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-fun 5806 This theorem is referenced by:  funprg  5854  funprgOLD  5855  funtpg  5856  funtpgOLD  5857  funtp  5859  funcnvpr  5864  funcnvtp  5865  funcnvqp  5866  funcnvqpOLD  5867  fnun  5911  fvun  6178  wfrlem13  7314  tfrlem10  7370  sbthlem7  7961  sbthlem8  7962  fodomr  7996  funsnfsupp  8182  axdc3lem4  9158  setsfun  15725  setsfun0  15726  strlemor1  15796  strleun  15799  bnj1421  30364
 Copyright terms: Public domain W3C validator