Theorem fnsnsplit

Description: Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015)

	Ref	Expression
Assertion	fnsnsplit	$$⊢\left(FFnA\wedge X\in A\right)\to F=\left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,F\left(X\right)⟩\right\}$$

Proof

Step	Hyp	Ref	Expression
1		fnresdm	$$⊢FFnA\to {F\upharpoonright }_A=F$$
2	1	adantr	$$⊢\left(FFnA\wedge X\in A\right)\to {F\upharpoonright }_A=F$$
3		resundi	$$⊢{F\upharpoonright }_{\left(\left(A\setminus \left\{X\right\}\right)\cup \left\{X\right\}\right)}=\left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right)\cup \left({F\upharpoonright }_{\left\{X\right\}}\right)$$
4		difsnid	$$⊢X\in A\to \left(A\setminus \left\{X\right\}\right)\cup \left\{X\right\}=A$$
5	4	adantl	$$⊢\left(FFnA\wedge X\in A\right)\to \left(A\setminus \left\{X\right\}\right)\cup \left\{X\right\}=A$$
6	5	reseq2d	$$⊢\left(FFnA\wedge X\in A\right)\to {F\upharpoonright }_{\left(\left(A\setminus \left\{X\right\}\right)\cup \left\{X\right\}\right)}={F\upharpoonright }_A$$
7		fnressn	$$⊢\left(FFnA\wedge X\in A\right)\to {F\upharpoonright }_{\left\{X\right\}}=\left\{⟨X,F\left(X\right)⟩\right\}$$
8	7	uneq2d	$$⊢\left(FFnA\wedge X\in A\right)\to \left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right)\cup \left({F\upharpoonright }_{\left\{X\right\}}\right)=\left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,F\left(X\right)⟩\right\}$$
9	3 6 8	3eqtr3a	$$⊢\left(FFnA\wedge X\in A\right)\to {F\upharpoonright }_A=\left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,F\left(X\right)⟩\right\}$$
10	2 9	eqtr3d	$$⊢\left(FFnA\wedge X\in A\right)\to F=\left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,F\left(X\right)⟩\right\}$$