Theorem fnun

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

	Ref	Expression
Assertion	fnun	|- ( ( ( F Fn A /\ G Fn B ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) Fn ( A u. B ) )

Proof

Step	Hyp	Ref	Expression
1		df-fn	|- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2		df-fn	|- ( G Fn B <-> ( Fun G /\ dom G = B ) )
3		ineq12	|- ( ( dom F = A /\ dom G = B ) -> ( dom F i^i dom G ) = ( A i^i B ) )
4	3	eqeq1d	|- ( ( dom F = A /\ dom G = B ) -> ( ( dom F i^i dom G ) = (/) <-> ( A i^i B ) = (/) ) )
5	4	anbi2d	|- ( ( dom F = A /\ dom G = B ) -> ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) <-> ( ( Fun F /\ Fun G ) /\ ( A i^i B ) = (/) ) ) )
6		funun	|- ( ( ( Fun F /\ Fun G ) /\ ( dom F i^i dom G ) = (/) ) -> Fun ( F u. G ) )
7	5 6	biimtrrdi	|- ( ( dom F = A /\ dom G = B ) -> ( ( ( Fun F /\ Fun G ) /\ ( A i^i B ) = (/) ) -> Fun ( F u. G ) ) )
8		dmun	|- dom ( F u. G ) = ( dom F u. dom G )
9		uneq12	|- ( ( dom F = A /\ dom G = B ) -> ( dom F u. dom G ) = ( A u. B ) )
10	8 9	eqtrid	|- ( ( dom F = A /\ dom G = B ) -> dom ( F u. G ) = ( A u. B ) )
11	7 10	jctird	|- ( ( dom F = A /\ dom G = B ) -> ( ( ( Fun F /\ Fun G ) /\ ( A i^i B ) = (/) ) -> ( Fun ( F u. G ) /\ dom ( F u. G ) = ( A u. B ) ) ) )
12		df-fn	|- ( ( F u. G ) Fn ( A u. B ) <-> ( Fun ( F u. G ) /\ dom ( F u. G ) = ( A u. B ) ) )
13	11 12	imbitrrdi	|- ( ( dom F = A /\ dom G = B ) -> ( ( ( Fun F /\ Fun G ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) Fn ( A u. B ) ) )
14	13	expd	|- ( ( dom F = A /\ dom G = B ) -> ( ( Fun F /\ Fun G ) -> ( ( A i^i B ) = (/) -> ( F u. G ) Fn ( A u. B ) ) ) )
15	14	impcom	|- ( ( ( Fun F /\ Fun G ) /\ ( dom F = A /\ dom G = B ) ) -> ( ( A i^i B ) = (/) -> ( F u. G ) Fn ( A u. B ) ) )
16	15	an4s	|- ( ( ( Fun F /\ dom F = A ) /\ ( Fun G /\ dom G = B ) ) -> ( ( A i^i B ) = (/) -> ( F u. G ) Fn ( A u. B ) ) )
17	1 2 16	syl2anb	|- ( ( F Fn A /\ G Fn B ) -> ( ( A i^i B ) = (/) -> ( F u. G ) Fn ( A u. B ) ) )
18	17	imp	|- ( ( ( F Fn A /\ G Fn B ) /\ ( A i^i B ) = (/) ) -> ( F u. G ) Fn ( A u. B ) )