Theorem funun 2700

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 2681	. . . . . 6 |- (Fun F -> Rel F)
2		funrel 2681	. . . . . 6 |- (Fun G -> Rel G)
3	1, 2	anim12i 268	. . . . 5 |- ((Fun F /\ Fun G) -> (Rel F /\ Rel G))
4		relun 2490	. . . . 5 |- (Rel (F u. G) <-> (Rel F /\ Rel G))
5	3, 4	sylibr 175	. . . 4 |- ((Fun F /\ Fun G) -> Rel (F u. G))
6	5	adantr 306	. . 3 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> Rel (F u. G))
7		disj1 1734	. . . . . . . . . . . . . 14 |- ((dom F i^i dom G) = (/) <-> A.x(x e. dom F -> -. x e. dom G))
8	7	biimp 133	. . . . . . . . . . . . 13 |- ((dom F i^i dom G) = (/) -> A.x(x e. dom F -> -. x e. dom G))
9	8	19.21bi 742	. . . . . . . . . . . 12 |- ((dom F i^i dom G) = (/) -> (x e. dom F -> -. x e. dom G))
10		imnan 207	. . . . . . . . . . . 12 |- ((x e. dom F -> -. x e. dom G) <-> -. (x e. dom F /\ x e. dom G))
11	9, 10	sylib 173	. . . . . . . . . . 11 |- ((dom F i^i dom G) = (/) -> -. (x e. dom F /\ x e. dom G))
12		visset 1350	. . . . . . . . . . . . 13 |- x e. V
13	12	opeldm 2534	. . . . . . . . . . . 12 |- (<.x, y>. e. F -> x e. dom F)
14	12	opeldm 2534	. . . . . . . . . . . 12 |- (<.x, z>. e. G -> x e. dom G)
15	13, 14	anim12i 268	. . . . . . . . . . 11 |- ((<.x, y>. e. F /\ <.x, z>. e. G) -> (x e. dom F /\ x e. dom G))
16	11, 15	nsyl 102	. . . . . . . . . 10 |- ((dom F i^i dom G) = (/) -> -. (<.x, y>. e. F /\ <.x, z>. e. G))
17		orel2 213	. . . . . . . . . 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 12	. . . . . . . . 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 83	. . . . . . . . . . . 12 |- ((dom F i^i dom G) = (/) -> (x e. dom G -> -. x e. dom F))
20		imnan 207	. . . . . . . . . . . 12 |- ((x e. dom G -> -. x e. dom F) <-> -. (x e. dom G /\ x e. dom F))
21	19, 20	sylib 173	. . . . . . . . . . 11 |- ((dom F i^i dom G) = (/) -> -. (x e. dom G /\ x e. dom F))
22	12	opeldm 2534	. . . . . . . . . . . 12 |- (<.x, y>. e. G -> x e. dom G)
23	12	opeldm 2534	. . . . . . . . . . . 12 |- (<.x, z>. e. F -> x e. dom F)
24	22, 23	anim12i 268	. . . . . . . . . . 11 |- ((<.x, y>. e. G /\ <.x, z>. e. F) -> (x e. dom G /\ x e. dom F))
25	21, 24	nsyl 102	. . . . . . . . . 10 |- ((dom F i^i dom G) = (/) -> -. (<.x, y>. e. G /\ <.x, z>. e. F))
26		orel1 212	. . . . . . . . . 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 12	. . . . . . . . 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 436	. . . . . . . 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 305	. . . . . . 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 1601	. . . . . . . . 9 |- (<.x, y>. e. (F u. G) <-> (<.x, y>. e. F \/ <.x, y>. e. G))
31		elun 1601	. . . . . . . . 9 |- (<.x, z>. e. (F u. G) <-> (<.x, z>. e. F \/ <.x, z>. e. G))
32	30, 31	anbi12i 369	. . . . . . . 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 459	. . . . . . . 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	bitr 151	. . . . . . 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 181	. . . . . 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 2676	. . . . . . . . . . 11 |- (Fun F <-> (Rel F /\ A.xA.yA.z((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z)))
37	36	pm3.27bd 263	. . . . . . . . . 10 |- (Fun F -> A.xA.yA.z((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z))
38	37	19.21bi 742	. . . . . . . . 9 |- (Fun F -> A.yA.z((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z))
39	38	19.21bbi 743	. . . . . . . 8 |- (Fun F -> ((<.x, y>. e. F /\ <.x, z>. e. F) -> y = z))
40		dffun4 2676	. . . . . . . . . . 11 |- (Fun G <-> (Rel G /\ A.xA.yA.z((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z)))
41	40	pm3.27bd 263	. . . . . . . . . 10 |- (Fun G -> A.xA.yA.z((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z))
42	41	19.21bi 742	. . . . . . . . 9 |- (Fun G -> A.yA.z((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z))
43	42	19.21bbi 743	. . . . . . . 8 |- (Fun G -> ((<.x, y>. e. G /\ <.x, z>. e. G) -> y = z))
44	39, 43	jaao 330	. . . . . . 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 306	. . . . . 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 943	. . . 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)) -> y = z))
48	47	19.21aivv 944	. . 3 |- (((Fun F /\ Fun G) /\ (dom F i^i dom G) = (/)) -> A.xA.yA.z((<.x, y>. e. (F u. G) /\ <.x