Theorem fresaun

Description: The union of two functions which agree on their common domain is a function. (Contributed by Stefan O'Rear, 9-Oct-2014)

	Ref	Expression
Assertion	fresaun	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left(F\cup G\right):A\cup B⟶C$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to F:A⟶C$$
2		inss1	$$⊢A\cap B\subseteq A$$
3		fssres	$$⊢\left(F:A⟶C\wedge A\cap B\subseteq A\right)\to \left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B⟶C$$
4	1 2 3	sylancl	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left({F\upharpoonright }_{\left(A\cap B\right)}\right):A\cap B⟶C$$
5		difss	$$⊢A\setminus B\subseteq A$$
6		fssres	$$⊢\left(F:A⟶C\wedge A\setminus B\subseteq A\right)\to \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B⟶C$$
7	1 5 6	sylancl	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left({F\upharpoonright }_{\left(A\setminus B\right)}\right):A\setminus B⟶C$$
8		simp2	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to G:B⟶C$$
9		difss	$$⊢B\setminus A\subseteq B$$
10		fssres	$$⊢\left(G:B⟶C\wedge B\setminus A\subseteq B\right)\to \left({G\upharpoonright }_{\left(B\setminus A\right)}\right):B\setminus A⟶C$$
11	8 9 10	sylancl	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left({G\upharpoonright }_{\left(B\setminus A\right)}\right):B\setminus A⟶C$$
12		indifdir	$$⊢\left(A\setminus B\right)\cap \left(B\setminus A\right)=\left(A\cap \left(B\setminus A\right)\right)\setminus \left(B\cap \left(B\setminus A\right)\right)$$
13		disjdif	$$⊢A\cap \left(B\setminus A\right)=\varnothing$$
14	13	difeq1i	$$⊢\left(A\cap \left(B\setminus A\right)\right)\setminus \left(B\cap \left(B\setminus A\right)\right)=\varnothing \setminus \left(B\cap \left(B\setminus A\right)\right)$$
15		0dif	$$⊢\varnothing \setminus \left(B\cap \left(B\setminus A\right)\right)=\varnothing$$
16	12 14 15	3eqtri	$$⊢\left(A\setminus B\right)\cap \left(B\setminus A\right)=\varnothing$$
17	16	a1i	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left(A\setminus B\right)\cap \left(B\setminus A\right)=\varnothing$$
18	7 11 17	fun2d	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)\cup \left({G\upharpoonright }_{\left(B\setminus A\right)}\right)\right):\left(A\setminus B\right)\cup \left(B\setminus A\right)⟶C$$
19		indi	$$⊢\left(A\cap B\right)\cap \left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)=\left(\left(A\cap B\right)\cap \left(A\setminus B\right)\right)\cup \left(\left(A\cap B\right)\cap \left(B\setminus A\right)\right)$$
20		inass	$$⊢\left(A\cap B\right)\cap \left(A\setminus B\right)=A\cap \left(B\cap \left(A\setminus B\right)\right)$$
21		disjdif	$$⊢B\cap \left(A\setminus B\right)=\varnothing$$
22	21	ineq2i	$$⊢A\cap \left(B\cap \left(A\setminus B\right)\right)=A\cap \varnothing$$
23		in0	$$⊢A\cap \varnothing =\varnothing$$
24	20 22 23	3eqtri	$$⊢\left(A\cap B\right)\cap \left(A\setminus B\right)=\varnothing$$
25		incom	$$⊢A\cap B=B\cap A$$
26	25	ineq1i	$$⊢\left(A\cap B\right)\cap \left(B\setminus A\right)=\left(B\cap A\right)\cap \left(B\setminus A\right)$$
27		inass	$$⊢\left(B\cap A\right)\cap \left(B\setminus A\right)=B\cap \left(A\cap \left(B\setminus A\right)\right)$$
28	13	ineq2i	$$⊢B\cap \left(A\cap \left(B\setminus A\right)\right)=B\cap \varnothing$$
29		in0	$$⊢B\cap \varnothing =\varnothing$$
30	27 28 29	3eqtri	$$⊢\left(B\cap A\right)\cap \left(B\setminus A\right)=\varnothing$$
31	26 30	eqtri	$$⊢\left(A\cap B\right)\cap \left(B\setminus A\right)=\varnothing$$
32	24 31	uneq12i	$$⊢\left(\left(A\cap B\right)\cap \left(A\setminus B\right)\right)\cup \left(\left(A\cap B\right)\cap \left(B\setminus A\right)\right)=\varnothing \cup \varnothing$$
33		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
34	19 32 33	3eqtri	$$⊢\left(A\cap B\right)\cap \left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)=\varnothing$$
35	34	a1i	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left(A\cap B\right)\cap \left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)=\varnothing$$
36	4 18 35	fun2d	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left(\left({F\upharpoonright }_{\left(A\cap B\right)}\right)\cup \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)\cup \left({G\upharpoonright }_{\left(B\setminus A\right)}\right)\right)\right):\left(A\cap B\right)\cup \left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)⟶C$$
37		un12	$$⊢\left(A\cap B\right)\cup \left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)=\left(A\setminus B\right)\cup \left(\left(A\cap B\right)\cup \left(B\setminus A\right)\right)$$
38	25	uneq1i	$$⊢\left(A\cap B\right)\cup \left(B\setminus A\right)=\left(B\cap A\right)\cup \left(B\setminus A\right)$$
39		inundif	$$⊢\left(B\cap A\right)\cup \left(B\setminus A\right)=B$$
40	38 39	eqtri	$$⊢\left(A\cap B\right)\cup \left(B\setminus A\right)=B$$
41	40	uneq2i	$$⊢\left(A\setminus B\right)\cup \left(\left(A\cap B\right)\cup \left(B\setminus A\right)\right)=\left(A\setminus B\right)\cup B$$
42		undif1	$$⊢\left(A\setminus B\right)\cup B=A\cup B$$
43	37 41 42	3eqtri	$$⊢\left(A\cap B\right)\cup \left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)=A\cup B$$
44	43	feq2i	$$⊢\left(\left({F\upharpoonright }_{\left(A\cap B\right)}\right)\cup \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)\cup \left({G\upharpoonright }_{\left(B\setminus A\right)}\right)\right)\right):\left(A\cap B\right)\cup \left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)⟶C\leftrightarrow \left(\left({F\upharpoonright }_{\left(A\cap B\right)}\right)\cup \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)\cup \left({G\upharpoonright }_{\left(B\setminus A\right)}\right)\right)\right):A\cup B⟶C$$
45		ffn	$$⊢F:A⟶C\to FFnA$$
46		ffn	$$⊢G:B⟶C\to GFnB$$
47		id	$$⊢{F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\to {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}$$
48		resasplit	$$⊢\left(FFnA\wedge GFnB\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to F\cup G=\left({F\upharpoonright }_{\left(A\cap B\right)}\right)\cup \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)\cup \left({G\upharpoonright }_{\left(B\setminus A\right)}\right)\right)$$
49	45 46 47 48	syl3an	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to F\cup G=\left({F\upharpoonright }_{\left(A\cap B\right)}\right)\cup \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)\cup \left({G\upharpoonright }_{\left(B\setminus A\right)}\right)\right)$$
50	49	feq1d	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left(\left(F\cup G\right):A\cup B⟶C\leftrightarrow \left(\left({F\upharpoonright }_{\left(A\cap B\right)}\right)\cup \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)\cup \left({G\upharpoonright }_{\left(B\setminus A\right)}\right)\right)\right):A\cup B⟶C\right)$$
51	44 50	bitr4id	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left(\left(\left({F\upharpoonright }_{\left(A\cap B\right)}\right)\cup \left(\left({F\upharpoonright }_{\left(A\setminus B\right)}\right)\cup \left({G\upharpoonright }_{\left(B\setminus A\right)}\right)\right)\right):\left(A\cap B\right)\cup \left(\left(A\setminus B\right)\cup \left(B\setminus A\right)\right)⟶C\leftrightarrow \left(F\cup G\right):A\cup B⟶C\right)$$
52	36 51	mpbid	$$⊢\left(F:A⟶C\wedge G:B⟶C\wedge {F\upharpoonright }_{\left(A\cap B\right)}={G\upharpoonright }_{\left(A\cap B\right)}\right)\to \left(F\cup G\right):A\cup B⟶C$$