Metamath Proof Explorer

Theorem fnun

Description: The union of two functions with disjoint domains. (Contributed by NM, 22-Sep-2004)

		Ref	Expression
	Assertion	fnun	$⊢ ((F Fn A \land G Fn B) \land A \cap B = \emptyset) \to (F \cup G) Fn (A \cup B)$

Proof

Step	Hyp	Ref	Expression
1		df-fn	$⊢ F Fn A \leftrightarrow (Fun F \land dom F = A)$
2		df-fn	$⊢ G Fn B \leftrightarrow (Fun G \land dom G = B)$
3		ineq12	$⊢ (dom F = A \land dom G = B) \to dom F \cap dom G = A \cap B$
4	3	eqeq1d	$⊢ (dom F = A \land dom G = B) \to (dom F \cap dom G = \emptyset \leftrightarrow A \cap B = \emptyset)$
5	4	anbi2d	$⊢ (dom F = A \land dom G = B) \to (((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \leftrightarrow ((Fun F \land Fun G) \land A \cap B = \emptyset))$
6		funun	$⊢ ((Fun F \land Fun G) \land dom F \cap dom G = \emptyset) \to Fun (F \cup G)$
7	5 6	syl6bir	$⊢ (dom F = A \land dom G = B) \to (((Fun F \land Fun G) \land A \cap B = \emptyset) \to Fun (F \cup G))$
8		dmun	$⊢ dom (F \cup G) = dom F \cup dom G$
9		uneq12	$⊢ (dom F = A \land dom G = B) \to dom F \cup dom G = A \cup B$
10	8 9	eqtrid	$⊢ (dom F = A \land dom G = B) \to dom (F \cup G) = A \cup B$
11	7 10	jctird	$⊢ (dom F = A \land dom G = B) \to (((Fun F \land Fun G) \land A \cap B = \emptyset) \to (Fun (F \cup G) \land dom (F \cup G) = A \cup B))$
12		df-fn	$⊢ (F \cup G) Fn (A \cup B) \leftrightarrow (Fun (F \cup G) \land dom (F \cup G) = A \cup B)$
13	11 12	syl6ibr	$⊢ (dom F = A \land dom G = B) \to (((Fun F \land Fun G) \land A \cap B = \emptyset) \to (F \cup G) Fn (A \cup B))$
14	13	expd	$⊢ (dom F = A \land dom G = B) \to ((Fun F \land Fun G) \to (A \cap B = \emptyset \to (F \cup G) Fn (A \cup B)))$
15	14	impcom	$⊢ ((Fun F \land Fun G) \land (dom F = A \land dom G = B)) \to (A \cap B = \emptyset \to (F \cup G) Fn (A \cup B))$
16	15	an4s	$⊢ ((Fun F \land dom F = A) \land (Fun G \land dom G = B)) \to (A \cap B = \emptyset \to (F \cup G) Fn (A \cup B))$
17	1 2 16	syl2anb	$⊢ (F Fn A \land G Fn B) \to (A \cap B = \emptyset \to (F \cup G) Fn (A \cup B))$
18	17	imp	$⊢ ((F Fn A \land G Fn B) \land A \cap B = \emptyset) \to (F \cup G) Fn (A \cup B)$