funun

Description: The union of functions with disjoint domains is a function. Theorem 4.6 of Monk1 p. 43. (Contributed by NM, 12-Aug-1994)

		Ref	Expression
	Assertion	funun	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to Fun (F \cup G)$

Proof

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun F \to Rel F$
2		funrel	$⊢ Fun G \to Rel G$
3	1 2	anim12i	$⊢ (Fun F \land Fun G) \to (Rel F \land Rel G)$
4		relun	$⊢ Rel (F \cup G) \leftrightarrow (Rel F \land Rel G)$
5	3 4	sylibr	$⊢ (Fun F \land Fun G) \to Rel (F \cup G)$
6	5	adantr	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to Rel (F \cup G)$
7		elun	$⊢ ⟨x, y⟩ \in (F \cup G) \leftrightarrow (⟨x, y⟩ \in F \lor ⟨x, y⟩ \in G)$
8		elun	$⊢ ⟨x, z⟩ \in (F \cup G) \leftrightarrow (⟨x, z⟩ \in F \lor ⟨x, z⟩ \in G)$
9	7 8	anbi12i	$⊢ (⟨x, y⟩ \in (F \cup G) \land ⟨x, z⟩ \in (F \cup G)) \leftrightarrow ((⟨x, y⟩ \in F \lor ⟨x, y⟩ \in G) \land (⟨x, z⟩ \in F \lor ⟨x, z⟩ \in G))$
10		anddi	$⊢ ((⟨x, y⟩ \in F \lor ⟨x, y⟩ \in G) \land (⟨x, z⟩ \in F \lor ⟨x, z⟩ \in G)) \leftrightarrow (((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)) \lor ((⟨x, y⟩ \in G \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G)))$
11	9 10	bitri	$⊢ (⟨x, y⟩ \in (F \cup G) \land ⟨x, z⟩ \in (F \cup G)) \leftrightarrow (((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)) \lor ((⟨x, y⟩ \in G \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G)))$
12		disj1	$⊢ dom F \cap dom G = \emptyset \leftrightarrow \forall x (x \in dom F \to \neg x \in dom G)$
13	12	biimpi	$⊢ dom F \cap dom G = \emptyset \to \forall x (x \in dom F \to \neg x \in dom G)$
14	13	19.21bi	$⊢ dom F \cap dom G = \emptyset \to (x \in dom F \to \neg x \in dom G)$
15		imnan	$⊢ (x \in dom F \to \neg x \in dom G) \leftrightarrow \neg (x \in dom F \land x \in dom G)$
16	14 15	sylib	$⊢ dom F \cap dom G = \emptyset \to \neg (x \in dom F \land x \in dom G)$
17		vex	$⊢ x \in V$
18		vex	$⊢ y \in V$
19	17 18	opeldm	$⊢ ⟨x, y⟩ \in F \to x \in dom F$
20		vex	$⊢ z \in V$
21	17 20	opeldm	$⊢ ⟨x, z⟩ \in G \to x \in dom G$
22	19 21	anim12i	$⊢ (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G) \to (x \in dom F \land x \in dom G)$
23	16 22	nsyl	$⊢ dom F \cap dom G = \emptyset \to \neg (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)$
24		orel2	$⊢ \neg (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G) \to (((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)) \to (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F))$
25	23 24	syl	$⊢ dom F \cap dom G = \emptyset \to (((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)) \to (⟨x, y⟩ \in F \land ⟨x, z⟩ \in F))$
26	14	con2d	$⊢ dom F \cap dom G = \emptyset \to (x \in dom G \to \neg x \in dom F)$
27		imnan	$⊢ (x \in dom G \to \neg x \in dom F) \leftrightarrow \neg (x \in dom G \land x \in dom F)$
28	26 27	sylib	$⊢ dom F \cap dom G = \emptyset \to \neg (x \in dom G \land x \in dom F)$
29	17 18	opeldm	$⊢ ⟨x, y⟩ \in G \to x \in dom G$
30	17 20	opeldm	$⊢ ⟨x, z⟩ \in F \to x \in dom F$
31	29 30	anim12i	$⊢ (⟨x, y⟩ \in G \land ⟨x, z⟩ \in F) \to (x \in dom G \land x \in dom F)$
32	28 31	nsyl	$⊢ dom F \cap dom G = \emptyset \to \neg (⟨x, y⟩ \in G \land ⟨x, z⟩ \in F)$
33		orel1	$⊢ \neg (⟨x, y⟩ \in G \land ⟨x, z⟩ \in F) \to (((⟨x, y⟩ \in G \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G)) \to (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G))$
34	32 33	syl	$⊢ dom F \cap dom G = \emptyset \to (((⟨x, y⟩ \in G \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G)) \to (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G))$
35	25 34	orim12d	$⊢ dom F \cap dom G = \emptyset \to ((((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)) \lor ((⟨x, y⟩ \in G \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G))) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G)))$
36	35	adantl	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to ((((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in F \land ⟨x, z⟩ \in G)) \lor ((⟨x, y⟩ \in G \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G))) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G)))$
37	11 36	syl5bi	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to ((⟨x, y⟩ \in (F \cup G) \land ⟨x, z⟩ \in (F \cup G)) \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G)))$
38		dffun4	$⊢ Fun F \leftrightarrow (Rel F \land \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z))$
39	38	simprbi	$⊢ Fun F \to \forall x \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
40	39	19.21bi	$⊢ Fun F \to \forall y \forall z ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
41	40	19.21bbi	$⊢ Fun F \to ((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \to y = z)$
42		dffun4	$⊢ Fun G \leftrightarrow (Rel G \land \forall x \forall y \forall z ((⟨x, y⟩ \in G \land ⟨x, z⟩ \in G) \to y = z))$
43	42	simprbi	$⊢ Fun G \to \forall x \forall y \forall z ((⟨x, y⟩ \in G \land ⟨x, z⟩ \in G) \to y = z)$
44	43	19.21bi	$⊢ Fun G \to \forall y \forall z ((⟨x, y⟩ \in G \land ⟨x, z⟩ \in G) \to y = z)$
45	44	19.21bbi	$⊢ Fun G \to ((⟨x, y⟩ \in G \land ⟨x, z⟩ \in G) \to y = z)$
46	41 45	jaao	$⊢ (Fun F \land Fun G) \to (((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G)) \to y = z)$
47	46	adantr	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to (((⟨x, y⟩ \in F \land ⟨x, z⟩ \in F) \lor (⟨x, y⟩ \in G \land ⟨x, z⟩ \in G)) \to y = z)$
48	37 47	syld	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to ((⟨x, y⟩ \in (F \cup G) \land ⟨x, z⟩ \in (F \cup G)) \to y = z)$
49	48	alrimiv	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to \forall z ((⟨x, y⟩ \in (F \cup G) \land ⟨x, z⟩ \in (F \cup G)) \to y = z)$
50	49	alrimivv	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to \forall x \forall y \forall z ((⟨x, y⟩ \in (F \cup G) \land ⟨x, z⟩ \in (F \cup G)) \to y = z)$
51		dffun4	$⊢ Fun (F \cup G) \leftrightarrow (Rel (F \cup G) \land \forall x \forall y \forall z ((⟨x, y⟩ \in (F \cup G) \land ⟨x, z⟩ \in (F \cup G)) \to y = z))$
52	6 50 51	sylanbrc	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to Fun (F \cup G)$

Metamath Proof Explorer

Theorem funun

Proof