Theorem funun 3629

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		funrel 3608	. . . . . 6 |- (Fun F -> Rel F)
2		funrel 3608	. . . . . 6 |- (Fun G -> Rel G)
3	1, 2	anim12i 331	. . . . 5 |- ((Fun F /\ Fun G) -> (Rel F /\ Rel G))
4		relun 3323	. . . . 5 |- (Rel (F u. G) <-> (Rel F /\ Rel G))
5	3, 4	sylibr 198	. . . 4 |- ((Fun F /\ Fun G) -> Rel (F u. G))
6	5	adantr 389	. . 3 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> Rel (F u. G))
7		disj1 2357	. . . . . . . . . . . . . 14 |- ((dom F i^i dom G) = (/) <-> A.x(x e. dom F -> -. x e. dom G))
8	7	biimpi 149	. . . . . . . . . . . . 13 |- ((dom F i^i dom G) = (/) -> A.x(x e. dom F -> -. x e. dom G))
9	8	19.21bi 1092	. . . . . . . . . . . 12 |- ((dom F i^i dom G) = (/) -> (x e. dom F -> -. x e. dom G))
10		imnan 240	. . . . . . . . . . . 12 |- ((x e. dom F -> -. x e. dom G) <-> -. (x e. dom F /\ x e. dom G))
11	9, 10	sylib 196	. . . . . . . . . . 11 |- ((dom F i^i dom G) = (/) -> -. (x e. dom F /\ x e. dom G))
12		visset 1851	. . . . . . . . . . . . 13 |- x e. V
13	12	opeldm 3378	. . . . . . . . . . . 12 |- (<.x, y>. e. F -> x e. dom F)
14	12	opeldm 3378	. . . . . . . . . . . 12 |- (<.x, z>. e. G -> x e. dom G)
15	13, 14	anim12i 331	. . . . . . . . . . 11 |- ((<.x, y>. e. F /\ <.x, z>. e. G) -> (x e. dom F /\ x e. dom G))
16	11, 15	nsyl 115	. . . . . . . . . 10 |- ((dom F i^i dom G) = (/) -> -. (<.x, y>. e. F /\ <.x, z>. e. G))
17		orel2 250	. . . . . . . . . 10 |- (-. (<.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)))
18	16, 17	syl 10	. . . . . . . . 9 |- ((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)))
19	9	con2d 91	. . . . . . . . . . . 12 |- ((dom F i^i dom G) = (/) -> (x e. dom G -> -. x e. dom F))
20		imnan 240	. . . . . . . . . . . 12 |- ((x e. dom G -> -. x e. dom F) <-> -. (x e. dom G /\ x e. dom F))
21	19, 20	sylib 196	. . . . . . . . . . 11 |- ((dom F i^i dom G) = (/) -> -. (x e. dom G /\ x e. dom F))
22	12	opeldm 3378	. . . . . . . . . . . 12 |- (<.x, y>. e. G -> x e. dom G)
23	12	opeldm 3378	. . . . . . . . . . . 12 |- (<.x, z>. e. F -> x e. dom F)
24	22, 23	anim12i 331	. . . . . . . . . . 11 |- ((<.x, y>. e. G /\ <.x, z>. e. F) -> (x e. dom G /\ x e. dom F))
25	21, 24	nsyl 115	. . . . . . . . . 10 |- ((dom F i^i dom G) = (/) -> -. (<.x, y>. e. G /\ <.x, z>. e. F))
26		orel1 249	. . . . . . . . . 10 |- (-. (<.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)))
27	25, 26	syl 10	. . . . . . . . 9 |- ((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)))
28	18, 27	orim12d 567	. . . . . . . 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. 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))))
29	28	adantl 388	. . . . . . 7 |- (((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))))
30		elun 2217	. . . . . . . . 9 |- (<.x, y>. e. (F u. G) <-> (<.x, y>. e. F \/ <.x, y>. e. G))
31		elun 2217	. . . . . . . . 9 |- (<.x, z>. e. (F u. G) <-> (<.x, z>. e. F \/ <.x, z>. e. G))
32	30, 31	anbi12i 484	. . . . . . . 8 |- ((<.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)))
33		anddi 609	. . . . . . . 8 |- (((<.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))))
34	32, 33	bitri 171	. . . . . . 7 |- ((<.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))))
35	29, 34	syl5ib 204	. . . . . 6 |- (((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))))
36		dffun4 3603	. . . . . . . . . . 11 |- (Fun F <-> (Rel F /\ A.xA.yA.z((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z)))
37	36	pm3.27bi 324	. . . . . . . . . 10 |- (Fun F -> A.xA.yA.z((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z))
38	37	19.21bi 1092	. . . . . . . . 9 |- (Fun F -> A.yA.z((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z))
39	38	19.21bbi 1093	. . . . . . . 8 |- (Fun F -> ((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z))
40		dffun4 3603	. . . . . . . . . . 11 |- (Fun G <-> (Rel G /\ A.xA.yA.z((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z)))
41	40	pm3.27bi 324	. . . . . . . . . 10 |- (Fun G -> A.xA.yA.z((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z))
42	41	19.21bi 1092	. . . . . . . . 9 |- (Fun G -> A.yA.z((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z))
43	42	19.21bbi 1093	. . . . . . . 8 |- (Fun G -> ((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z))
44	39, 43	jaao 427	. . . . . . 7 |- ((Fun F /\ Fun G) -> (((<.x, y>. e. F /\ <.x, z>. e. F) \/ (<.x, y>. e. G /\ <.x, z>. e. G)) -> y = z))
45	44	adantr 389	. . . . . 6 |- (((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))
46	35, 45	syld 27	. . . . 5 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> ((<.x, y>. e. (F u. G) /\ <.x, z>. e. (F u. G)) -> y = z))
47	46	19.21aiv 1319	. . . 4 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> A.z((<.x, y>. e. (F u. G) /\ <.x, z>. e. (F u. G