Theorem fdmdifeqresdif

Description: The restriction of a conditional mapping to function values of a function having a domain which is a difference with a singleton equals this function. (Contributed by AV, 23-Apr-2019)

	Ref	Expression
Hypothesis	fdmdifeqresdif.f	$$⊢F=\left(x\in D⟼if\left(x=Y,X,G\left(x\right)\right)\right)$$
Assertion	fdmdifeqresdif	$$⊢G:D\setminus \left\{Y\right\}⟶R\to G={F\upharpoonright }_{\left(D\setminus \left\{Y\right\}\right)}$$

Proof

Step	Hyp	Ref	Expression
1		fdmdifeqresdif.f	$$⊢F=\left(x\in D⟼if\left(x=Y,X,G\left(x\right)\right)\right)$$
2		eldifsnneq	$$⊢x\in \left(D\setminus \left\{Y\right\}\right)\to \neg x=Y$$
3	2	adantl	$$⊢\left(G:D\setminus \left\{Y\right\}⟶R\wedge x\in \left(D\setminus \left\{Y\right\}\right)\right)\to \neg x=Y$$
4	3	iffalsed	$$⊢\left(G:D\setminus \left\{Y\right\}⟶R\wedge x\in \left(D\setminus \left\{Y\right\}\right)\right)\to if\left(x=Y,X,G\left(x\right)\right)=G\left(x\right)$$
5	4	mpteq2dva	$$⊢G:D\setminus \left\{Y\right\}⟶R\to \left(x\in \left(D\setminus \left\{Y\right\}\right)⟼if\left(x=Y,X,G\left(x\right)\right)\right)=\left(x\in \left(D\setminus \left\{Y\right\}\right)⟼G\left(x\right)\right)$$
6	1	reseq1i	$$⊢{F\upharpoonright }_{\left(D\setminus \left\{Y\right\}\right)}={\left(x\in D⟼if\left(x=Y,X,G\left(x\right)\right)\right)\upharpoonright }_{\left(D\setminus \left\{Y\right\}\right)}$$
7		difssd	$$⊢G:D\setminus \left\{Y\right\}⟶R\to D\setminus \left\{Y\right\}\subseteq D$$
8	7	resmptd	$$⊢G:D\setminus \left\{Y\right\}⟶R\to {\left(x\in D⟼if\left(x=Y,X,G\left(x\right)\right)\right)\upharpoonright }_{\left(D\setminus \left\{Y\right\}\right)}=\left(x\in \left(D\setminus \left\{Y\right\}\right)⟼if\left(x=Y,X,G\left(x\right)\right)\right)$$
9	6 8	syl5eq	$$⊢G:D\setminus \left\{Y\right\}⟶R\to {F\upharpoonright }_{\left(D\setminus \left\{Y\right\}\right)}=\left(x\in \left(D\setminus \left\{Y\right\}\right)⟼if\left(x=Y,X,G\left(x\right)\right)\right)$$
10		ffn	$$⊢G:D\setminus \left\{Y\right\}⟶R\to GFn\left(D\setminus \left\{Y\right\}\right)$$
11		dffn5	$$⊢GFn\left(D\setminus \left\{Y\right\}\right)\leftrightarrow G=\left(x\in \left(D\setminus \left\{Y\right\}\right)⟼G\left(x\right)\right)$$
12	10 11	sylib	$$⊢G:D\setminus \left\{Y\right\}⟶R\to G=\left(x\in \left(D\setminus \left\{Y\right\}\right)⟼G\left(x\right)\right)$$
13	5 9 12	3eqtr4rd	$$⊢G:D\setminus \left\{Y\right\}⟶R\to G={F\upharpoonright }_{\left(D\setminus \left\{Y\right\}\right)}$$