Theorem funun 4870

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 x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funrel 4845	. . . . 5 ⊢ (Fun 𝐹 → Rel 𝐹)
2		funrel 4845	. . . . 5 ⊢ (Fun 𝐺 → Rel 𝐺)
3	1, 2	anim12i 321	. . . 4 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (Rel 𝐹 ∧ Rel 𝐺))
4		relun 4381	. . . 4 ⊢ (Rel (𝐹 ∪ 𝐺) ↔ (Rel 𝐹 ∧ Rel 𝐺))
5	3, 4	sylibr 137	. . 3 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Rel (𝐹 ∪ 𝐺))
6	5	adantr 261	. 2 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Rel (𝐹 ∪ 𝐺))
7		elun 3061	. . . . . . . 8 ⊢ (⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ↔ (⟨x, y⟩ ∈ 𝐹 ∨ ⟨x, y⟩ ∈ 𝐺))
8		elun 3061	. . . . . . . 8 ⊢ (⟨x, z⟩ ∈ (𝐹 ∪ 𝐺) ↔ (⟨x, z⟩ ∈ 𝐹 ∨ ⟨x, z⟩ ∈ 𝐺))
9	7, 8	anbi12i 436	. . . . . . 7 ⊢ ((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) ↔ ((⟨x, y⟩ ∈ 𝐹 ∨ ⟨x, y⟩ ∈ 𝐺) ∧ (⟨x, z⟩ ∈ 𝐹 ∨ ⟨x, z⟩ ∈ 𝐺)))
10		anddi 722	. . . . . . 7 ⊢ (((⟨x, y⟩ ∈ 𝐹 ∨ ⟨x, y⟩ ∈ 𝐺) ∧ (⟨x, z⟩ ∈ 𝐹 ∨ ⟨x, z⟩ ∈ 𝐺)) ↔ (((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺)) ∨ ((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺))))
11	9, 10	bitri 173	. . . . . 6 ⊢ ((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) ↔ (((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺)) ∨ ((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺))))
12		disj1 3247	. . . . . . . . . . . . 13 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ ∀x(x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺))
13	12	biimpi 113	. . . . . . . . . . . 12 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ∀x(x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺))
14	13	19.21bi 1432	. . . . . . . . . . 11 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺))
15		imnan 611	. . . . . . . . . . 11 ⊢ ((x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺) ↔ ¬ (x ∈ dom 𝐹 ∧ x ∈ dom 𝐺))
16	14, 15	sylib 127	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (x ∈ dom 𝐹 ∧ x ∈ dom 𝐺))
17		vex 2538	. . . . . . . . . . . 12 ⊢ x ∈ V
18		vex 2538	. . . . . . . . . . . 12 ⊢ y ∈ V
19	17, 18	opeldm 4465	. . . . . . . . . . 11 ⊢ (⟨x, y⟩ ∈ 𝐹 → x ∈ dom 𝐹)
20		vex 2538	. . . . . . . . . . . 12 ⊢ z ∈ V
21	17, 20	opeldm 4465	. . . . . . . . . . 11 ⊢ (⟨x, z⟩ ∈ 𝐺 → x ∈ dom 𝐺)
22	19, 21	anim12i 321	. . . . . . . . . 10 ⊢ ((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺) → (x ∈ dom 𝐹 ∧ x ∈ dom 𝐺))
23	16, 22	nsyl 546	. . . . . . . . 9 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺))
24		orel2 632	. . . . . . . . 9 ⊢ (¬ (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺) → (((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺)) → (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹)))
25	23, 24	syl 14	. . . . . . . 8 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺)) → (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹)))
26	14	con2d 542	. . . . . . . . . . 11 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (x ∈ dom 𝐺 → ¬ x ∈ dom 𝐹))
27		imnan 611	. . . . . . . . . . 11 ⊢ ((x ∈ dom 𝐺 → ¬ x ∈ dom 𝐹) ↔ ¬ (x ∈ dom 𝐺 ∧ x ∈ dom 𝐹))
28	26, 27	sylib 127	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (x ∈ dom 𝐺 ∧ x ∈ dom 𝐹))
29	17, 18	opeldm 4465	. . . . . . . . . . 11 ⊢ (⟨x, y⟩ ∈ 𝐺 → x ∈ dom 𝐺)
30	17, 20	opeldm 4465	. . . . . . . . . . 11 ⊢ (⟨x, z⟩ ∈ 𝐹 → x ∈ dom 𝐹)
31	29, 30	anim12i 321	. . . . . . . . . 10 ⊢ ((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹) → (x ∈ dom 𝐺 ∧ x ∈ dom 𝐹))
32	28, 31	nsyl 546	. . . . . . . . 9 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹))
33		orel1 631	. . . . . . . . 9 ⊢ (¬ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹) → (((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺)) → (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺)))
34	32, 33	syl 14	. . . . . . . 8 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺)) → (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺)))
35	25, 34	orim12d 687	. . . . . . 7 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ((((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺)) ∨ ((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺))) → ((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺))))
36	35	adantl 262	. . . . . 6 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺)) ∨ ((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺))) → ((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺))))
37	11, 36	syl5bi 141	. . . . 5 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) → ((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺))))
38		dffun4 4840	. . . . . . . . . 10 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀x∀y∀z((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) → y = z)))
39	38	simprbi 260	. . . . . . . . 9 ⊢ (Fun 𝐹 → ∀x∀y∀z((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) → y = z))
40	39	19.21bi 1432	. . . . . . . 8 ⊢ (Fun 𝐹 → ∀y∀z((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) → y = z))
41	40	19.21bbi 1433	. . . . . . 7 ⊢ (Fun 𝐹 → ((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) → y = z))
42		dffun4 4840	. . . . . . . . . 10 ⊢ (Fun 𝐺 ↔ (Rel 𝐺 ∧ ∀x∀y∀z((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺) → y = z)))
43	42	simprbi 260	. . . . . . . . 9 ⊢ (Fun 𝐺 → ∀x∀y∀z((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺) → y = z))
44	43	19.21bi 1432	. . . . . . . 8 ⊢ (Fun 𝐺 → ∀y∀z((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺) → y = z))
45	44	19.21bbi 1433	. . . . . . 7 ⊢ (Fun 𝐺 → ((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺) → y = z))
46	41, 45	jaao 626	. . . . . 6 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺)) → y = z))
47	46	adantr 261	. . . . 5 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → (((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) ∨ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺)) → y = z))
48	37, 47	syld 40	. . . 4 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) → y = z))
49	48	alrimiv 1736	. . 3 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀z((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) → y = z))
50	49	alrimivv 1737	. 2 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀x∀y∀z((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) → y = z))
51		dffun4 4840	. 2 ⊢ (Fun (𝐹 ∪ 𝐺) ↔ (Rel (𝐹 ∪ 𝐺) ∧ ∀x∀y∀z((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) → y = z)))
52	6, 50, 51	sylanbrc 396	1 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 616  ∀wal 1226   = wceq 1228   ∈ wcel 1374   ∪ cun 2892   ∩ cin 2893  ∅c0 3201  ⟨cop 3353  dom cdm 4272  Rel wrel 4277  Fun wfun 4823

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3849  ax-pow 3901  ax-pr 3918

This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-eu 1885  df-mo 1886  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2289  df-v 2537  df-dif 2897  df-un 2899  df-in 2901  df-ss 2908  df-nul 3202  df-pw 3336  df-sn 3356  df-pr 3357  df-op 3359  df-br 3739  df-opab 3793  df-id 4004  df-rel 4279  df-cnv 4280  df-co 4281  df-dm 4282  df-fun 4831

This theorem is referenced by:  funprg  4875  funtpg  4876  funtp  4878  fnun  4931  fvun1  5164