Theorem funun 4462

Description: The union of functions with disjoint domains is a function. Theorem 4.6 of [Monk1] p. 43.

Assertion

Ref	Expression
funun	|- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> Fun (F u. G))

Proof of Theorem funun

Step	Hyp	Ref	Expression
1		dffun4 4433	. 2 |- (Fun (F u. G) <-> (Rel (F u. G) /\ A.xA.yA.z((<.x, y>. e. (F u. G) /\ <.x, z>. e. (F u. G)) -> y = z)))
2		funrel 4438	. . . . 5 |- (Fun F -> Rel F)
3		funrel 4438	. . . . 5 |- (Fun G -> Rel G)
4	2, 3	anim12i 360	. . . 4 |- ((Fun F /\ Fun G) -> (Rel F /\ Rel G))
5		relun 4097	. . . 4 |- (Rel (F u. G) <-> (Rel F /\ Rel G))
6	4, 5	sylibr 217	. . 3 |- ((Fun F /\ Fun G) -> Rel (F u. G))
7	6	adantr 425	. 2 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> Rel (F u. G))
8		disj1 2915	. . . . . . . . . . . . 13 |- ((dom F i^i dom G) = (/) <-> A.x(x e. dom F -> -. x e. dom G))
9	8	biimpi 168	. . . . . . . . . . . 12 |- ((dom F i^i dom G) = (/) -> A.x(x e. dom F -> -. x e. dom G))
10	9	19.21bi 1408	. . . . . . . . . . 11 |- ((dom F i^i dom G) = (/) -> (x e. dom F -> -. x e. dom G))
11		imnan 261	. . . . . . . . . . 11 |- ((x e. dom F -> -. x e. dom G) <-> -. (x e. dom F /\ x e. dom G))
12	10, 11	sylib 215	. . . . . . . . . 10 |- ((dom F i^i dom G) = (/) -> -. (x e. dom F /\ x e. dom G))
13		visset 2295	. . . . . . . . . . . 12 |- x e. _V
14	13	opeldm 4160	. . . . . . . . . . 11 |- (<.x, y>. e. F -> x e. dom F)
15	13	opeldm 4160	. . . . . . . . . . 11 |- (<.x, z>. e. G -> x e. dom G)
16	14, 15	anim12i 360	. . . . . . . . . 10 |- ((<.x, y>. e. F /\ <.x, z>. e. G) -> (x e. dom F /\ x e. dom G))
17	12, 16	nsyl 131	. . . . . . . . 9 |- ((dom F i^i dom G) = (/) -> -. (<.x, y>. e. F /\ <.x, z>. e. G))
18		orel2 272	. . . . . . . . 9 |- (-. (<.x, y>. e. F /\ <.x, z>. e. G) -> (((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. F /\ <.x, z>. e. G)) -> (<.x, y>. e. F /\ <.x, z>. e. F)))
19	17, 18	syl 12	. . . . . . . 8 |- ((dom F i^i dom G) = (/) -> (((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. F /\ <.x, z>. e. G)) -> (<.x, y>. e. F /\ <.x, z>. e. F)))
20	10	con2d 107	. . . . . . . . . . 11 |- ((dom F i^i dom G) = (/) -> (x e. dom G -> -. x e. dom F))
21		imnan 261	. . . . . . . . . . 11 |- ((x e. dom G -> -. x e. dom F) <-> -. (x e. dom G /\ x e. dom F))
22	20, 21	sylib 215	. . . . . . . . . 10 |- ((dom F i^i dom G) = (/) -> -. (x e. dom G /\ x e. dom F))
23	13	opeldm 4160	. . . . . . . . . . 11 |- (<.x, y>. e. G -> x e. dom G)
24	13	opeldm 4160	. . . . . . . . . . 11 |- (<.x, z>. e. F -> x e. dom F)
25	23, 24	anim12i 360	. . . . . . . . . 10 |- ((<.x, y>. e. G /\ <.x, z>. e. F) -> (x e. dom G /\ x e. dom F))
26	22, 25	nsyl 131	. . . . . . . . 9 |- ((dom F i^i dom G) = (/) -> -. (<.x, y>. e. G /\ <.x, z>. e. F))
27		orel1 271	. . . . . . . . 9 |- (-. (<.x, y>. e. G /\ <.x, z>. e. F) -> (((<.x, y>. e. G /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G)) -> (<.x, y>. e. G /\ <.x, z>. e. G)))
28	26, 27	syl 12	. . . . . . . 8 |- ((dom F i^i dom G) = (/) -> (((<.x, y>. e. G /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G)) -> (<.x, y>. e. G /\ <.x, z>. e. G)))
29	19, 28	orim12d 624	. . . . . . 7 |- ((dom F i^i dom G) = (/) -> ((((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. F /\ <.x, z>. e. G)) \/ ((<.x, y>. e. G /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G))) -> ((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G))))
30	29	adantl 424	. . . . . 6 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> ((((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. F /\ <.x, z>. e. G)) \/ ((<.x, y>. e. G /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G))) -> ((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G))))
31		elun 2741	. . . . . . . 8 |- (<.x, y>. e. (F u. G) <-> (<.x, y>. e. F \/ <.x, y>. e. G))
32		elun 2741	. . . . . . . 8 |- (<.x, z>. e. (F u. G) <-> (<.x, z>. e. F \/ <.x, z>. e. G))
33	31, 32	anbi12i 540	. . . . . . 7 |- ((<.x, y>. e. (F u. G) /\ <.x, z>. e. (F u. G)) <-> ((<.x, y>. e. F \/ <.x, y>. e. G) /\ (<.x, z>. e. F \/ <.x, z>. e. G)))
34		anddi 668	. . . . . . 7 |- (((<.x, y>. e. F \/ <.x, y>. e. G) /\ (<.x, z>. e. F \/ <.x, z>. e. G)) <-> (((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. F /\ <.x, z>. e. G)) \/ ((<.x, y>. e. G /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G))))
35	33, 34	bitri 190	. . . . . 6 |- ((<.x, y>. e. (F u. G) /\ <.x, z>. e. (F u. G)) <-> (((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. F /\ <.x, z>. e. G)) \/ ((<.x, y>. e. G /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G))))
36	30, 35	syl5ib 223	. . . . 5 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> ((<.x, y>. e. (F u. G) /\ <.x, z>. e. (F u. G)) -> ((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G))))
37		dffun4 4433	. . . . . . . . . 10 |- (Fun F <-> (Rel F /\ A.xA.yA.z((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z)))
38	37	simprbi 353	. . . . . . . . 9 |- (Fun F -> A.xA.yA.z((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z))
39	38	19.21bi 1408	. . . . . . . 8 |- (Fun F -> A.yA.z((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z))
40	39	19.21bbi 1409	. . . . . . 7 |- (Fun F -> ((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z))
41		dffun4 4433	. . . . . . . . . 10 |- (Fun G <-> (Rel G /\ A.xA.yA.z((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z)))
42	41	simprbi 353	. . . . . . . . 9 |- (Fun G -> A.xA.yA.z((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z))
43	42	19.21bi 1408	. . . . . . . 8 |- (Fun G -> A.yA.z((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z))
44	43	19.21bbi 1409	. . . . . . 7 |- (Fun G -> ((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z))
45	40, 44	jaao 472	. . . . . 6 |- ((Fun F /\ Fun G) -> (((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G)) -> y = z))
46	45	adantr 425	. . . . 5 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> (((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G)) -> y = z))
47	36, 46	syld 30	. . . 4 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> ((<.x, y>. e. (F u. G) /\ <.x, z>. e. (F u. G)) -> y = z))
48	47	19.21aiv 1664	. . 3 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> A.z((<.x, y>. e. (F u. G) /\ <.x, z>. e. (F u. G)) -> y = z))
49	48	19.21aivv 1665	. 2 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> A.xA.yA.z((<.x, y>. e. (F u. G) /\ <.x, z>. e. (F u. G)) -> y = z))
50	1, 7, 49	sylanbrc 527	1 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> Fun (F u. G))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300   u. cun 2591   i^i cin 2592  (/)c0 2875  <.cop 3046  dom cdm 3986  Rel wrel 3991  Fun wfun 3992

This theorem is referenced by:  funprg 4466  funtp 4468  fnun 4520  tfrlem10 5128  sbthlem7 5516  sbthlem8 5517  fodomr 5547  bnj1421 13532  wfrlem13 13969  valfunun 14460  repfuntw 14502

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-br 3339  df-opab 3396  df-id 3586  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-fun 4008

Copyright terms: Public domain