Theorem fsnunres

Description: Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015)

	Ref	Expression
Assertion	fsnunres	$$⊢\left(FFnS\wedge \neg X\in S\right)\to {\left(F\cup \left\{⟨X,Y⟩\right\}\right)\upharpoonright }_S=F$$

Proof

Step	Hyp	Ref	Expression
1		fnresdm	$$⊢FFnS\to {F\upharpoonright }_S=F$$
2	1	adantr	$$⊢\left(FFnS\wedge \neg X\in S\right)\to {F\upharpoonright }_S=F$$
3		ressnop0	$$⊢\neg X\in S\to {\left\{⟨X,Y⟩\right\}\upharpoonright }_S=\varnothing$$
4	3	adantl	$$⊢\left(FFnS\wedge \neg X\in S\right)\to {\left\{⟨X,Y⟩\right\}\upharpoonright }_S=\varnothing$$
5	2 4	uneq12d	$$⊢\left(FFnS\wedge \neg X\in S\right)\to \left({F\upharpoonright }_S\right)\cup \left({\left\{⟨X,Y⟩\right\}\upharpoonright }_S\right)=F\cup \varnothing$$
6		resundir	$$⊢{\left(F\cup \left\{⟨X,Y⟩\right\}\right)\upharpoonright }_S=\left({F\upharpoonright }_S\right)\cup \left({\left\{⟨X,Y⟩\right\}\upharpoonright }_S\right)$$
7		un0	$$⊢F\cup \varnothing =F$$
8	7	eqcomi	$$⊢F=F\cup \varnothing$$
9	5 6 8	3eqtr4g	$$⊢\left(FFnS\wedge \neg X\in S\right)\to {\left(F\cup \left\{⟨X,Y⟩\right\}\right)\upharpoonright }_S=F$$