Theorem funun 6545

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 6516	. . . . 5 ⊢ (Fun 𝐹 → Rel 𝐹)
2		funrel 6516	. . . . 5 ⊢ (Fun 𝐺 → Rel 𝐺)
3	1, 2	anim12i 614	. . . 4 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (Rel 𝐹 ∧ Rel 𝐺))
4		relun 5767	. . . 4 ⊢ (Rel (𝐹 ∪ 𝐺) ↔ (Rel 𝐹 ∧ Rel 𝐺))
5	3, 4	sylibr 234	. . 3 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → Rel (𝐹 ∪ 𝐺))
6	5	adantr 480	. 2 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Rel (𝐹 ∪ 𝐺))
7		elun 4094	. . . . . . . 8 ⊢ (⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ↔ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺))
8		elun 4094	. . . . . . . 8 ⊢ (⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺) ↔ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
9	7, 8	anbi12i 629	. . . . . . 7 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) ↔ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
10		anddi 1013	. . . . . . 7 ⊢ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑦⟩ ∈ 𝐺) ∧ (⟨𝑥, 𝑧⟩ ∈ 𝐹 ∨ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
11	9, 10	bitri 275	. . . . . 6 ⊢ ((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) ↔ (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
12		disj1 4393	. . . . . . . . . . . . 13 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ ↔ ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
13	12	biimpi 216	. . . . . . . . . . . 12 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ∀𝑥(𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
14	13	19.21bi 2197	. . . . . . . . . . 11 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺))
15		imnan 399	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ dom 𝐹 → ¬ 𝑥 ∈ dom 𝐺) ↔ ¬ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺))
16	14, 15	sylib 218	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺))
17		vex 3434	. . . . . . . . . . . 12 ⊢ 𝑥 ∈ V
18		vex 3434	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
19	17, 18	opeldm 5863	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐹 → 𝑥 ∈ dom 𝐹)
20		vex 3434	. . . . . . . . . . . 12 ⊢ 𝑧 ∈ V
21	17, 20	opeldm 5863	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺)
22	19, 21	anim12i 614	. . . . . . . . . 10 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (𝑥 ∈ dom 𝐹 ∧ 𝑥 ∈ dom 𝐺))
23	16, 22	nsyl 140	. . . . . . . . 9 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))
24		orel2 891	. . . . . . . . 9 ⊢ (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
25	23, 24	syl 17	. . . . . . . 8 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹)))
26	14	con2d 134	. . . . . . . . . . 11 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹))
27		imnan 399	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ dom 𝐺 → ¬ 𝑥 ∈ dom 𝐹) ↔ ¬ (𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹))
28	26, 27	sylib 218	. . . . . . . . . 10 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹))
29	17, 18	opeldm 5863	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐺 → 𝑥 ∈ dom 𝐺)
30	17, 20	opeldm 5863	. . . . . . . . . . 11 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝐹 → 𝑥 ∈ dom 𝐹)
31	29, 30	anim12i 614	. . . . . . . . . 10 ⊢ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (𝑥 ∈ dom 𝐺 ∧ 𝑥 ∈ dom 𝐹))
32	28, 31	nsyl 140	. . . . . . . . 9 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹))
33		orel1 889	. . . . . . . . 9 ⊢ (¬ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
34	32, 33	syl 17	. . . . . . . 8 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → (((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)))
35	25, 34	orim12d 967	. . . . . . 7 ⊢ ((dom 𝐹 ∩ dom 𝐺) = ∅ → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
36	35	adantl 481	. . . . . 6 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) ∨ ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
37	11, 36	biimtrid 242	. . . . 5 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺))))
38		dffun4 6512	. . . . . . . . . 10 ⊢ (Fun 𝐹 ↔ (Rel 𝐹 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧)))
39	38	simprbi 497	. . . . . . . . 9 ⊢ (Fun 𝐹 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
40	39	19.21bi 2197	. . . . . . . 8 ⊢ (Fun 𝐹 → ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
41	40	19.21bbi 2198	. . . . . . 7 ⊢ (Fun 𝐹 → ((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) → 𝑦 = 𝑧))
42		dffun4 6512	. . . . . . . . . 10 ⊢ (Fun 𝐺 ↔ (Rel 𝐺 ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧)))
43	42	simprbi 497	. . . . . . . . 9 ⊢ (Fun 𝐺 → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
44	43	19.21bi 2197	. . . . . . . 8 ⊢ (Fun 𝐺 → ∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
45	44	19.21bbi 2198	. . . . . . 7 ⊢ (Fun 𝐺 → ((⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺) → 𝑦 = 𝑧))
46	41, 45	jaao 957	. . . . . 6 ⊢ ((Fun 𝐹 ∧ Fun 𝐺) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
47	46	adantr 480	. . . . 5 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → (((⟨𝑥, 𝑦⟩ ∈ 𝐹 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐹) ∨ (⟨𝑥, 𝑦⟩ ∈ 𝐺 ∧ ⟨𝑥, 𝑧⟩ ∈ 𝐺)) → 𝑦 = 𝑧))
48	37, 47	syld 47	. . . 4 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧))
49	48	alrimiv 1929	. . 3 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧))
50	49	alrimivv 1930	. 2 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧))
51		dffun4 6512	. 2 ⊢ (Fun (𝐹 ∪ 𝐺) ↔ (Rel (𝐹 ∪ 𝐺) ∧ ∀𝑥∀𝑦∀𝑧((⟨𝑥, 𝑦⟩ ∈ (𝐹 ∪ 𝐺) ∧ ⟨𝑥, 𝑧⟩ ∈ (𝐹 ∪ 𝐺)) → 𝑦 = 𝑧)))
52	6, 50, 51	sylanbrc 584	1 ⊢ (((Fun 𝐹 ∧ Fun 𝐺) ∧ (dom 𝐹 ∩ dom 𝐺) = ∅) → Fun (𝐹 ∪ 𝐺))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 848  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ∪ cun 3888   ∩ cin 3889  ∅c0 4274  ⟨cop 4574  dom cdm 5631  Rel wrel 5636  Fun wfun 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-pr 5376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6501

This theorem is referenced by:  funprg  6553  funtpg  6554  funtp  6556  funcnvpr  6561  funcnvtp  6562  funcnvqp  6563  fnun  6613  fvun  6931  tfrlem10  8326  sbthlem7  9031  sbthlem8  9032  fodomr  9066  fodomfir  9238  funsnfsupp  9305  axdc3lem4  10375  strleun  17127  setsfun  17141  setsfun0  17142  cnfldfunALT  21367  noextend  27630  noextendseq  27631  bnj1421  35184  satffunlem1  35589  satffunlem2  35590