Theorem fsets

Description: The structure replacement function is a function. (Contributed by SO, 12-Jul-2018)

	Ref	Expression
Assertion	fsets	$$⊢\left(\left(F\in V\wedge F:A⟶B\right)\wedge X\in A\wedge Y\in B\right)\to \left(F\mathrm{sSet}⟨X,Y⟩\right):A⟶B$$

Proof

Step	Hyp	Ref	Expression
1		difss	$$⊢A\setminus \left\{X\right\}\subseteq A$$
2		fssres	$$⊢\left(F:A⟶B\wedge A\setminus \left\{X\right\}\subseteq A\right)\to \left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right):A\setminus \left\{X\right\}⟶B$$
3	1 2	mpan2	$$⊢F:A⟶B\to \left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right):A\setminus \left\{X\right\}⟶B$$
4		resres	$$⊢{\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}={F\upharpoonright }_{\left(A\cap \left(\mathrm{V}\setminus \left\{X\right\}\right)\right)}$$
5		invdif	$$⊢A\cap \left(\mathrm{V}\setminus \left\{X\right\}\right)=A\setminus \left\{X\right\}$$
6	5	reseq2i	$$⊢{F\upharpoonright }_{\left(A\cap \left(\mathrm{V}\setminus \left\{X\right\}\right)\right)}={F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}$$
7	4 6	eqtri	$$⊢{\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}={F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}$$
8		ffn	$$⊢F:A⟶B\to FFnA$$
9		fnresdm	$$⊢FFnA\to {F\upharpoonright }_A=F$$
10	8 9	syl	$$⊢F:A⟶B\to {F\upharpoonright }_A=F$$
11	10	reseq1d	$$⊢F:A⟶B\to {\left({F\upharpoonright }_A\right)\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}={F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}$$
12	7 11	syl5reqr	$$⊢F:A⟶B\to {F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}={F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}$$
13	12	feq1d	$$⊢F:A⟶B\to \left(\left({F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}\right):A\setminus \left\{X\right\}⟶B\leftrightarrow \left({F\upharpoonright }_{\left(A\setminus \left\{X\right\}\right)}\right):A\setminus \left\{X\right\}⟶B\right)$$
14	3 13	mpbird	$$⊢F:A⟶B\to \left({F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}\right):A\setminus \left\{X\right\}⟶B$$
15	14	adantl	$$⊢\left(F\in V\wedge F:A⟶B\right)\to \left({F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}\right):A\setminus \left\{X\right\}⟶B$$
16		fsnunf2	$$⊢\left(\left({F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}\right):A\setminus \left\{X\right\}⟶B\wedge X\in A\wedge Y\in B\right)\to \left(\left({F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,Y⟩\right\}\right):A⟶B$$
17	15 16	syl3an1	$$⊢\left(\left(F\in V\wedge F:A⟶B\right)\wedge X\in A\wedge Y\in B\right)\to \left(\left({F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,Y⟩\right\}\right):A⟶B$$
18		simp1l	$$⊢\left(\left(F\in V\wedge F:A⟶B\right)\wedge X\in A\wedge Y\in B\right)\to F\in V$$
19		simp3	$$⊢\left(\left(F\in V\wedge F:A⟶B\right)\wedge X\in A\wedge Y\in B\right)\to Y\in B$$
20		setsval	$$⊢\left(F\in V\wedge Y\in B\right)\to F\mathrm{sSet}⟨X,Y⟩=\left({F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,Y⟩\right\}$$
21	20	feq1d	$$⊢\left(F\in V\wedge Y\in B\right)\to \left(\left(F\mathrm{sSet}⟨X,Y⟩\right):A⟶B\leftrightarrow \left(\left({F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,Y⟩\right\}\right):A⟶B\right)$$
22	18 19 21	syl2anc	$$⊢\left(\left(F\in V\wedge F:A⟶B\right)\wedge X\in A\wedge Y\in B\right)\to \left(\left(F\mathrm{sSet}⟨X,Y⟩\right):A⟶B\leftrightarrow \left(\left({F\upharpoonright }_{\left(\mathrm{V}\setminus \left\{X\right\}\right)}\right)\cup \left\{⟨X,Y⟩\right\}\right):A⟶B\right)$$
23	17 22	mpbird	$$⊢\left(\left(F\in V\wedge F:A⟶B\right)\wedge X\in A\wedge Y\in B\right)\to \left(F\mathrm{sSet}⟨X,Y⟩\right):A⟶B$$