Theorem fnun 3669

Description: The union of two functions with disjoint domains.

Assertion

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

Proof of Theorem fnun

Step	Hyp	Ref	Expression
1		ineq12 2256	. . . . . . . . . . 11 |- ((dom F = A /\ dom G = B) -> (dom F i^i dom G) = (A i^i B))
2	1	eqeq1d 1520	. . . . . . . . . 10 |- ((dom F = A /\ dom G = B) -> ((dom F i^i dom G) = (/) <-> (A i^i B) = (/)))
3	2	anbi2d 618	. . . . . . . . 9 |- ((dom F = A /\ dom G = B) -> (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) <-> ((Fun F /\ Fun G) /\ (A i^i B) = (/))))
4		funun 3629	. . . . . . . . 9 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> Fun (F u. G))
5	3, 4	syl6bir 213	. . . . . . . 8 |- ((dom F = A /\ dom G = B) -> (((Fun F /\ Fun G) /\ (A i^i B) = (/)) -> Fun (F u. G)))
6		uneq12 2223	. . . . . . . . 9 |- ((dom F = A /\ dom G = B) -> (dom F u. dom G) = (A u. B))
7		dmun 3381	. . . . . . . . 9 |- dom ( F u. G) = (dom F u. dom G)
8	6, 7	syl5eq 1556	. . . . . . . 8 |- ((dom F = A /\ dom G = B) -> dom ( F u. G) = (A u. B))
9	5, 8	jctird 604	. . . . . . 7 |- ((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))))
10		df-fn 3248	. . . . . . 7 |- ((F u. G) Fn (A u. B) <-> (Fun (F u. G) /\ dom ( F u. G) = (A u. B)))
11	9, 10	syl6ibr 211	. . . . . 6 |- ((dom F = A /\ dom G = B) -> (((Fun F /\ Fun G) /\ (A i^i B) = (/)) -> (F u. G) Fn (A u. B)))
12	11	exp3a 374	. . . . 5 |- ((dom F = A /\ dom G = B) -> ((Fun F /\ Fun G) -> ((A i^i B) = (/) -> (F u. G) Fn (A u. B))))
13	12	impcom 349	. . . 4 |- (((Fun F /\ Fun G) /\ (dom F = A /\ dom G = B)) -> ((A i^i B) = (/) -> (F u. G) Fn (A u. B)))
14	13	an4s 510	. . 3 |- (((Fun F /\ dom F = A) /\ (Fun G /\ dom G = B)) -> ((A i^i B) = (/) -> (F u. G) Fn (A u. B)))
15		df-fn 3248	. . 3 |- (F Fn A <-> (Fun F /\ dom F = A))
16		df-fn 3248	. . 3 |- (G Fn B <-> (Fun G /\ dom G = B))
17	14, 15, 16	syl2anb 457	. 2 |- ((F Fn A /\ G Fn B) -> ((A i^i B) = (/) -> (F u. G) Fn (A u. B)))
18	17	imp 348	1 |- (((F Fn A /\ G Fn B) /\ (A i^i B) = (/)) -> (F u. G) Fn (A u. B))

Syntax hints:   -> wi 3   /\ wa 221   = wceq 988   u. cun 2089   i^i cin 2090  (/)c0 2324  dom cdm 3225  Fun wfun 3231   Fn wfn 3232

This theorem is referenced by:  fun 3716  f1oun 3782

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-11 999  ax-12 1000  ax-13 1001  ax-14 1002  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494  ax-sep 2754  ax-pow 2794  ax-pr 2832

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-eu 1415  df-mo 1416  df-clab 1500  df-cleq 1505  df-clel 1508  df-ne 1624  df-ral 1687  df-v 1850  df-dif 2093  df-un 2094  df-in 2095  df-ss 2097  df-nul 2325  df-pw 2447  df-sn 2457  df-pr 2458  df-op 2461  df-br 2670  df-opab 2718  df-id 2889  df-rel 3240  df-cnv 3241  df-co 3242  df-dm 3243  df-fun 3247  df-fn 3248

Copyright terms: Public domain