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

Theorem funun 5920
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 5893 . . . . 5 (Fun 𝐹 → Rel 𝐹)
2 funrel 5893 . . . . 5 (Fun 𝐺 → Rel 𝐺)
31, 2anim12i 589 . . . 4 ((Fun 𝐹 ∧ Fun 𝐺) → (Rel 𝐹 ∧ Rel 𝐺))
4 relun 5225 . . . 4 (Rel (𝐹𝐺) ↔ (Rel 𝐹 ∧ Rel 𝐺))
53, 4sylibr 224 . . 3 ((Fun 𝐹 ∧ Fun 𝐺) → Rel (𝐹𝐺))
65adantr 481 . 2 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Rel (𝐹𝐺))
7 elun 3745 . . . . . . . 8 (⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
8 elun 3745 . . . . . . . 8 (⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
97, 8anbi12i 732 . . . . . . 7 ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
10 anddi 913 . . . . . . 7 (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
119, 10bitri 264 . . . . . 6 ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
12 disj1 4010 . . . . . . . . . . . . 13 ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
1312biimpi 206 . . . . . . . . . . . 12 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
141319.21bi 2057 . . . . . . . . . . 11 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
15 imnan 438 . . . . . . . . . . 11 ((𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺) ↔ ¬ (𝑥 ∈ dom 𝐹𝑥 ∈ dom 𝐺))
1614, 15sylib 208 . . . . . . . . . 10 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐹𝑥 ∈ dom 𝐺))
17 vex 3198 . . . . . . . . . . . 12 𝑥 ∈ V
18 vex 3198 . . . . . . . . . . . 12 𝑦 ∈ V
1917, 18opeldm 5317 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐹𝑥 ∈ dom 𝐹)
20 vex 3198 . . . . . . . . . . . 12 𝑧 ∈ V
2117, 20opeldm 5317 . . . . . . . . . . 11 (⟨𝑥, 𝑧⟩ ∈ 𝐺𝑥 ∈ dom 𝐺)
2219, 21anim12i 589 . . . . . . . . . 10 ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (𝑥 ∈ dom 𝐹𝑥 ∈ dom 𝐺))
2316, 22nsyl 135 . . . . . . . . 9 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
24 orel2 398 . . . . . . . . 9 (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
2523, 24syl 17 . . . . . . . 8 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
2614con2d 129 . . . . . . . . . . 11 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹))
27 imnan 438 . . . . . . . . . . 11 ((𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹) ↔ ¬ (𝑥 ∈ dom 𝐺𝑥 ∈ dom 𝐹))
2826, 27sylib 208 . . . . . . . . . 10 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐺𝑥 ∈ dom 𝐹))
2917, 18opeldm 5317 . . . . . . . . . . 11 (⟨𝑥, 𝑦⟩ ∈ 𝐺𝑥 ∈ dom 𝐺)
3017, 20opeldm 5317 . . . . . . . . . . 11 (⟨𝑥, 𝑧⟩ ∈ 𝐹𝑥 ∈ dom 𝐹)
3129, 30anim12i 589 . . . . . . . . . 10 ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑥 ∈ dom 𝐺𝑥 ∈ dom 𝐹))
3228, 31nsyl 135 . . . . . . . . 9 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
33 orel1 397 . . . . . . . . 9 (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
3432, 33syl 17 . . . . . . . 8 ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
3525, 34orim12d 882 . . . . . . 7 ((dom 𝐹 ∩ dom 𝐺) = ∅ → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
3635adantl 482 . . . . . 6 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
3711, 36syl5bi 232 . . . . 5 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
38 dffun4 5888 . . . . . . . . . 10 (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
3938simprbi 480 . . . . . . . . 9 (Fun 𝐹 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
403919.21bi 2057 . . . . . . . 8 (Fun 𝐹 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
414019.21bbi 2058 . . . . . . 7 (Fun 𝐹 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
42 dffun4 5888 . . . . . . . . . 10 (Fun 𝐺 ↔ (Rel 𝐺 ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧)))
4342simprbi 480 . . . . . . . . 9 (Fun 𝐺 → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
444319.21bi 2057 . . . . . . . 8 (Fun 𝐺 → ∀𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
454419.21bbi 2058 . . . . . . 7 (Fun 𝐺 → ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
4641, 45jaao 531 . . . . . 6 ((Fun 𝐹 ∧ Fun 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
4746adantr 481 . . . . 5 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
4837, 47syld 47 . . . 4 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧))
4948alrimiv 1853 . . 3 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧))
5049alrimivv 1854 . 2 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧))
51 dffun4 5888 . 2 (Fun (𝐹𝐺) ↔ (Rel (𝐹𝐺) ∧ ∀𝑥𝑦𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹𝐺)) → 𝑦 = 𝑧)))
526, 50, 51sylanbrc 697 1 (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹𝐺))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wo 383  wa 384  wal 1479   = wceq 1481  wcel 1988  cun 3565  cin 3566  c0 3907  cop 4174  dom cdm 5104  Rel wrel 5109  Fun wfun 5870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-id 5014  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-fun 5878
This theorem is referenced by:  funprg  5928  funprgOLD  5929  funtpg  5930  funtpgOLD  5931  funtp  5933  funcnvpr  5938  funcnvtp  5939  funcnvqp  5940  funcnvqpOLD  5941  fnun  5985  fvun  6255  wfrlem13  7412  tfrlem10  7468  sbthlem7  8061  sbthlem8  8062  fodomr  8096  funsnfsupp  8284  axdc3lem4  9260  setsfun  15874  setsfun0  15875  strlemor1OLD  15950  strleun  15953  cnfldfun  19739  bnj1421  31084  noextend  31793  noextendseq  31794
  Copyright terms: Public domain W3C validator