This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fun

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

		Ref	Expression
	Assertion	fun	$⊢ ((F : A ⟶ C \land G : B ⟶ D) \land A \cap B = \emptyset) \to (F \cup G) : A \cup B ⟶ C \cup D$

Proof

Step	Hyp	Ref	Expression
1		fnun	$⊢ ((F Fn A \land G Fn B) \land A \cap B = \emptyset) \to (F \cup G) Fn (A \cup B)$
2	1	expcom	$⊢ A \cap B = \emptyset \to ((F Fn A \land G Fn B) \to (F \cup G) Fn (A \cup B))$
3		rnun	$⊢ ran (F \cup G) = ran F \cup ran G$
4		unss12	$⊢ (ran F \subseteq C \land ran G \subseteq D) \to ran F \cup ran G \subseteq C \cup D$
5	3 4	eqsstrid	$⊢ (ran F \subseteq C \land ran G \subseteq D) \to ran (F \cup G) \subseteq C \cup D$
6	2 5	anim12d1	$⊢ A \cap B = \emptyset \to (((F Fn A \land G Fn B) \land (ran F \subseteq C \land ran G \subseteq D)) \to ((F \cup G) Fn (A \cup B) \land ran (F \cup G) \subseteq C \cup D))$
7		df-f	$⊢ F : A ⟶ C \leftrightarrow (F Fn A \land ran F \subseteq C)$
8		df-f	$⊢ G : B ⟶ D \leftrightarrow (G Fn B \land ran G \subseteq D)$
9	7 8	anbi12i	$⊢ (F : A ⟶ C \land G : B ⟶ D) \leftrightarrow ((F Fn A \land ran F \subseteq C) \land (G Fn B \land ran G \subseteq D))$
10		an4	$⊢ ((F Fn A \land ran F \subseteq C) \land (G Fn B \land ran G \subseteq D)) \leftrightarrow ((F Fn A \land G Fn B) \land (ran F \subseteq C \land ran G \subseteq D))$
11	9 10	bitri	$⊢ (F : A ⟶ C \land G : B ⟶ D) \leftrightarrow ((F Fn A \land G Fn B) \land (ran F \subseteq C \land ran G \subseteq D))$
12		df-f	$⊢ (F \cup G) : A \cup B ⟶ C \cup D \leftrightarrow ((F \cup G) Fn (A \cup B) \land ran (F \cup G) \subseteq C \cup D)$
13	6 11 12	3imtr4g	$⊢ A \cap B = \emptyset \to ((F : A ⟶ C \land G : B ⟶ D) \to (F \cup G) : A \cup B ⟶ C \cup D)$
14	13	impcom	$⊢ ((F : A ⟶ C \land G : B ⟶ D) \land A \cap B = \emptyset) \to (F \cup G) : A \cup B ⟶ C \cup D$