Theorem fun2

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

	Ref	Expression
Assertion	fun2	$$⊢\left(\left(F:A⟶C\wedge G:B⟶C\right)\wedge A\cap B=\varnothing \right)\to \left(F\cup G\right):A\cup B⟶C$$

Proof

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