Theorem funun 5162

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.

Step	Hyp	Ref	Expression
1		funrel 5135	. . . . 5 ⊢ (Fun 𝐹 → Rel 𝐹)
2		funrel 5135	. . . . 5 ⊢ (Fun 𝐺 → Rel 𝐺)
3	1, 2	anim12i 336	. . . 4 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (Rel 𝐹 ∧ Rel 𝐺))
4		relun 4651	. . . 4 ⊢ (Rel (𝐹 ∪ 𝐺) ↔ (Rel 𝐹 ∧ Rel 𝐺))
5	3, 4	sylibr 133	. . 3 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Rel (𝐹 ∪ 𝐺))
6	5	adantr 274	. 2 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Rel (𝐹 ∪ 𝐺))
7		elun 3212	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
8		elun 3212	. . . . . . . 8 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
9	7, 8	anbi12i 455	. . . . . . 7 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
10		anddi 810	. . . . . . 7 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
11	9, 10	bitri 183	. . . . . 6 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
12		disj1 3408	. . . . . . . . . . . . 13 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
13	12	biimpi 119	. . . . . . . . . . . 12 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
14	13	19.21bi 1537	. . . . . . . . . . 11 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
15		imnan 679	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺) ↔ ¬ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺))
16	14, 15	sylib 121	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺))
17		vex 2684	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
18		vex 2684	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
19	17, 18	opeldm 4737	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐹 → 𝑥 ∈ dom 𝐹)
20		vex 2684	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
21	17, 20	opeldm 4737	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺)
22	19, 21	anim12i 336	. . . . . . . . . 10 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺))
23	16, 22	nsyl 617	. . . . . . . . 9 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
24		orel2 715	. . . . . . . . 9 ⊢ (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
25	23, 24	syl 14	. . . . . . . 8 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
26	14	con2d 613	. . . . . . . . . . 11 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹))
27		imnan 679	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹) ↔ ¬ (𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹))
28	26, 27	sylib 121	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹))
29	17, 18	opeldm 4737	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺)
30	17, 20	opeldm 4737	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝐹 → 𝑥 ∈ dom 𝐹)
31	29, 30	anim12i 336	. . . . . . . . . 10 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹))
32	28, 31	nsyl 617	. . . . . . . . 9 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
33		orel1 714	. . . . . . . . 9 ⊢ (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
34	32, 33	syl 14	. . . . . . . 8 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
35	25, 34	orim12d 775	. . . . . . 7 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
36	35	adantl 275	. . . . . 6 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
37	11, 36	syl5bi 151	. . . . 5 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
38		dffun4 5129	. . . . . . . . . 10 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
39	38	simprbi 273	. . . . . . . . 9 ⊢ (Fun 𝐹 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
40	39	19.21bi 1537	. . . . . . . 8 ⊢ (Fun 𝐹 → ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
41	40	19.21bbi 1538	. . . . . . 7 ⊢ (Fun 𝐹 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
42		dffun4 5129	. . . . . . . . . 10 ⊢ (Fun 𝐺 ↔ (Rel 𝐺 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧)))
43	42	simprbi 273	. . . . . . . . 9 ⊢ (Fun 𝐺 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
44	43	19.21bi 1537	. . . . . . . 8 ⊢ (Fun 𝐺 → ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
45	44	19.21bbi 1538	. . . . . . 7 ⊢ (Fun 𝐺 → ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
46	41, 45	jaao 708	. . . . . 6 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
47	46	adantr 274	. . . . 5 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
48	37, 47	syld 45	. . . 4 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧))
49	48	alrimiv 1846	. . 3 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧))
50	49	alrimivv 1847	. 2 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧))
51		dffun4 5129	. 2 ⊢ (Fun (𝐹 ∪ 𝐺) ↔ (Rel (𝐹 ∪ 𝐺) ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧)))
52	6, 50, 51	sylanbrc 413	1 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 697  ∀wal 1329   = wceq 1331   ∈ wcel 1480   ∪ cun 3064   ∩ cin 3065  ∅c0 3358  ⟨cop 3525  dom cdm 4534  Rel wrel 4539  Fun wfun 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-pr 4126

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ral 2419  df-v 2683  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-nul 3359  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-br 3925  df-opab 3985  df-id 4210  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-fun 5120

This theorem is referenced by:  funprg  5168  funtpg  5169  funtp  5171  fnun  5224  fvun1  5480  sbthlem7  6844  sbthlemi8  6845  casefun  6963  caseinj  6967  djufun  6982  djuinj  6984  exmidfodomrlemim  7050  setsfun  11983  setsfun0  11984  strleund  12036  strleun  12037