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

Metamath Proof Explorer

Theorem fun2

Description: The union of two functions with disjoint domains. (Contributed by Mario Carneiro, 12-Mar-2015)

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

Step	Hyp	Ref	Expression
1		fun	$⊢ ((F : A ⟶ C \land G : B ⟶ C) \land A \cap B = \emptyset) \to (F \cup G) : A \cup B ⟶ C \cup C$
2		unidm	$⊢ C \cup C = C$
3		feq3	$⊢ C \cup C = C \to ((F \cup G) : A \cup B ⟶ C \cup C \leftrightarrow (F \cup G) : A \cup B ⟶ C)$
4	2 3	ax-mp	$⊢ (F \cup G) : A \cup B ⟶ C \cup C \leftrightarrow (F \cup G) : A \cup B ⟶ C$
5	1 4	sylib	$⊢ ((F : A ⟶ C \land G : B ⟶ C) \land A \cap B = \emptyset) \to (F \cup G) : A \cup B ⟶ C$