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 /\ G : B --> C ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) : ( A u. B ) --> C )

Proof

Step	Hyp	Ref	Expression
1		fun	|- ( ( ( F : A --> C /\ G : B --> C ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) : ( A u. B ) --> ( C u. C ) )
2		unidm	|- ( C u. C ) = C
3		feq3	|- ( ( C u. C ) = C -> ( ( F u. G ) : ( A u. B ) --> ( C u. C ) <-> ( F u. G ) : ( A u. B ) --> C ) )
4	2 3	ax-mp	|- ( ( F u. G ) : ( A u. B ) --> ( C u. C ) <-> ( F u. G ) : ( A u. B ) --> C )
5	1 4	sylib	|- ( ( ( F : A --> C /\ G : B --> C ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) : ( A u. B ) --> C )