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

Theorem funun 6597
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 6568 . . . . 5 (Fun 𝐹 → Rel 𝐹)
2 funrel 6568 . . . . 5 (Fun 𝐺 → Rel 𝐺)
31, 2anim12i 611 . . . 4 ((Fun 𝐹 ∧ Fun 𝐺) → (Rel 𝐹 ∧ Rel 𝐺))
4 relun 5809 . . . 4 (Rel (𝐹𝐺) ↔ (Rel 𝐹 ∧ Rel 𝐺))
53, 4sylibr 233 . . 3 ((Fun 𝐹 ∧ Fun 𝐺) → Rel (𝐹𝐺))
65adantr 479 . 2 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Rel (𝐹𝐺))
7 elun 4145 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
8 elun 4145 . . . . . . . 8 (⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
97, 8anbi12i 626 . . . . . . 7 ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
10 anddi 1008 . . . . . . 7 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
119, 10bitri 274 . . . . . 6 ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
12 disj1 4446 . . . . . . . . . . . . 13 ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
1312biimpi 215 . . . . . . . . . . . 12 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
141319.21bi 2178 . . . . . . . . . . 11 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
15 imnan 398 . . . . . . . . . . 11 ((𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺) ↔ ¬ (𝑥 ∈ dom 𝐹𝑥 ∈ dom 𝐺))
1614, 15sylib 217 . . . . . . . . . 10 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐹𝑥 ∈ dom 𝐺))
17 vex 3466 . . . . . . . . . . . 12 𝑥 ∈ V
18 vex 3466 . . . . . . . . . . . 12 𝑦 ∈ V
1917, 18opeldm 5906 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐹𝑥 ∈ dom 𝐹)
20 vex 3466 . . . . . . . . . . . 12 𝑧 ∈ V
2117, 20opeldm 5906 . . . . . . . . . . 11 (⟨𝑥, 𝑧⟩ ∈ 𝐺𝑥 ∈ dom 𝐺)
2219, 21anim12i 611 . . . . . . . . . 10 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (𝑥 ∈ dom 𝐹𝑥 ∈ dom 𝐺))
2316, 22nsyl 140 . . . . . . . . 9 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
24 orel2 888 . . . . . . . . 9 (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
2523, 24syl 17 . . . . . . . 8 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
2614con2d 134 . . . . . . . . . . 11 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹))
27 imnan 398 . . . . . . . . . . 11 ((𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹) ↔ ¬ (𝑥 ∈ dom 𝐺𝑥 ∈ dom 𝐹))
2826, 27sylib 217 . . . . . . . . . 10 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐺𝑥 ∈ dom 𝐹))
2917, 18opeldm 5906 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐺𝑥 ∈ dom 𝐺)
3017, 20opeldm 5906 . . . . . . . . . . 11 (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥 ∈ dom 𝐹)
3129, 30anim12i 611 . . . . . . . . . 10 ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑥 ∈ dom 𝐺𝑥 ∈ dom 𝐹))
3228, 31nsyl 140 . . . . . . . . 9 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
33 orel1 886 . . . . . . . . 9 (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
3432, 33syl 17 . . . . . . . 8 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
3525, 34orim12d 962 . . . . . . 7 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
3635adantl 480 . . . . . 6 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
3711, 36biimtrid 241 . . . . 5 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
38 dffun4 6562 . . . . . . . . . 10 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
3938simprbi 495 . . . . . . . . 9 (Fun 𝐹 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
403919.21bi 2178 . . . . . . . 8 (Fun 𝐹 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
414019.21bbi 2179 . . . . . . 7 (Fun 𝐹 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
42 dffun4 6562 . . . . . . . . . 10 (Fun 𝐺 ↔ (Rel 𝐺 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧)))
4342simprbi 495 . . . . . . . . 9 (Fun 𝐺 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
444319.21bi 2178 . . . . . . . 8 (Fun 𝐺 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
454419.21bbi 2179 . . . . . . 7 (Fun 𝐺 → ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
4641, 45jaao 952 . . . . . 6 ((Fun 𝐹 ∧ Fun 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
4746adantr 479 . . . . 5 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
4837, 47syld 47 . . . 4 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧))
4948alrimiv 1923 . . 3 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧))
5049alrimivv 1924 . 2 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧))
51 dffun4 6562 . 2 (Fun (𝐹𝐺) ↔ (Rel (𝐹𝐺) ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧)))
526, 50, 51sylanbrc 581 1 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wo 845  wal 1532   = wceq 1534  wcel 2099  cun 3944  cin 3945  c0 4322  cop 4629  dom cdm 5674  Rel wrel 5679  Fun wfun 6540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-12 2167  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4323  df-if 4524  df-sn 4624  df-pr 4626  df-op 4630  df-br 5146  df-opab 5208  df-id 5572  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-fun 6548
This theorem is referenced by:  funprg  6605  funtpg  6606  funtp  6608  funcnvpr  6613  funcnvtp  6614  funcnvqp  6615  fnun  6666  fvun  6984  wfrlem13OLD  8343  tfrlem10  8409  sbthlem7  9119  sbthlem8  9120  fodomr  9158  fodomfir  9363  funsnfsupp  9428  axdc3lem4  10487  strleun  17154  setsfun  17168  setsfun0  17169  cnfldfunALT  21354  cnfldfunALTOLD  21367  cnfldfunALTOLDOLD  21368  noextend  27693  noextendseq  27694  bnj1421  34900  satffunlem1  35248  satffunlem2  35249
  Copyright terms: Public domain W3C validator