Theorem funun 4887

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 4862	. . . . 5 ⊢ (Fun 𝐹 → Rel 𝐹)
2		funrel 4862	. . . . 5 ⊢ (Fun 𝐺 → Rel 𝐺)
3	1, 2	anim12i 321	. . . 4 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (Rel 𝐹 ∧ Rel 𝐺))
4		relun 4397	. . . 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 3078	. . . . . . . 8 ⊢ (⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ↔ (⟨x, y⟩ ∈ 𝐹 ∨ ⟨x, y⟩ ∈ 𝐺))
8		elun 3078	. . . . . . . 8 ⊢ (⟨x, z⟩ ∈ (𝐹 ∪ 𝐺) ↔ (⟨x, z⟩ ∈ 𝐹 ∨ ⟨x, z⟩ ∈ 𝐺))
9	7, 8	anbi12i 433	. . . . . . 7 ⊢ ((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) ↔ ((⟨x, y⟩ ∈ 𝐹 ∨ ⟨x, y⟩ ∈ 𝐺) ∧ (⟨x, z⟩ ∈ 𝐹 ∨ ⟨x, z⟩ ∈ 𝐺)))
10		anddi 733	. . . . . . 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 3264	. . . . . . . . . . . . 13 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ ∀x(x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺))
13	12	biimpi 113	. . . . . . . . . . . 12 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ∀x(x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺))
14	13	19.21bi 1447	. . . . . . . . . . 11 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺))
15		imnan 623	. . . . . . . . . . 11 ⊢ ((x ∈ dom 𝐹 → ¬ x ∈ dom 𝐺) ↔ ¬ (x ∈ dom 𝐹 ∧ x ∈ dom 𝐺))
16	14, 15	sylib 127	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (x ∈ dom 𝐹 ∧ x ∈ dom 𝐺))
17		vex 2554	. . . . . . . . . . . 12 ⊢ x ∈ V
18		vex 2554	. . . . . . . . . . . 12 ⊢ y ∈ V
19	17, 18	opeldm 4481	. . . . . . . . . . 11 ⊢ (⟨x, y⟩ ∈ 𝐹 → x ∈ dom 𝐹)
20		vex 2554	. . . . . . . . . . . 12 ⊢ z ∈ V
21	17, 20	opeldm 4481	. . . . . . . . . . 11 ⊢ (⟨x, z⟩ ∈ 𝐺 → x ∈ dom 𝐺)
22	19, 21	anim12i 321	. . . . . . . . . 10 ⊢ ((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺) → (x ∈ dom 𝐹 ∧ x ∈ dom 𝐺))
23	16, 22	nsyl 558	. . . . . . . . 9 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐺))
24		orel2 644	. . . . . . . . 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 554	. . . . . . . . . . 11 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (x ∈ dom 𝐺 → ¬ x ∈ dom 𝐹))
27		imnan 623	. . . . . . . . . . 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 4481	. . . . . . . . . . 11 ⊢ (⟨x, y⟩ ∈ 𝐺 → x ∈ dom 𝐺)
30	17, 20	opeldm 4481	. . . . . . . . . . 11 ⊢ (⟨x, z⟩ ∈ 𝐹 → x ∈ dom 𝐹)
31	29, 30	anim12i 321	. . . . . . . . . 10 ⊢ ((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹) → (x ∈ dom 𝐺 ∧ x ∈ dom 𝐹))
32	28, 31	nsyl 558	. . . . . . . . 9 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐹))
33		orel1 643	. . . . . . . . 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 699	. . . . . . 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 4856	. . . . . . . . . 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 1447	. . . . . . . 8 ⊢ (Fun 𝐹 → ∀y∀z((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) → y = z))
41	40	19.21bbi 1448	. . . . . . 7 ⊢ (Fun 𝐹 → ((⟨x, y⟩ ∈ 𝐹 ∧ ⟨x, z⟩ ∈ 𝐹) → y = z))
42		dffun4 4856	. . . . . . . . . 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 1447	. . . . . . . 8 ⊢ (Fun 𝐺 → ∀y∀z((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺) → y = z))
45	44	19.21bbi 1448	. . . . . . 7 ⊢ (Fun 𝐺 → ((⟨x, y⟩ ∈ 𝐺 ∧ ⟨x, z⟩ ∈ 𝐺) → y = z))
46	41, 45	jaao 638	. . . . . 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 1751	. . 3 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀z((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) → y = z))
50	49	alrimivv 1752	. 2 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀x∀y∀z((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) → y = z))
51		dffun4 4856	. 2 ⊢ (Fun (𝐹 ∪ 𝐺) ↔ (Rel (𝐹 ∪ 𝐺) ∧ ∀x∀y∀z((⟨x, y⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨x, z⟩ ∈ (𝐹 ∪ 𝐺)) → y = z)))
52	6, 50, 51	sylanbrc 394	1 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 628  ∀wal 1240   = wceq 1242   ∈ wcel 1390   ∪ cun 2909   ∩ cin 2910  ∅c0 3218  ⟨cop 3370  dom cdm 4288  Rel wrel 4293  Fun wfun 4839

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 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-id 4021  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-fun 4847

This theorem is referenced by:  funprg  4892  funtpg  4893  funtp  4895  fnun  4948  fvun1  5182