Theorem fsnunf2

Description: Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015)

	Ref	Expression
Assertion	fsnunf2	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge X\in S\wedge Y\in T\right)\to \left(F\cup \left\{⟨X,Y⟩\right\}\right):S⟶T$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge X\in S\wedge Y\in T\right)\to F:S\setminus \left\{X\right\}⟶T$$
2		simp2	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge X\in S\wedge Y\in T\right)\to X\in S$$
3		neldifsnd	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge X\in S\wedge Y\in T\right)\to \neg X\in \left(S\setminus \left\{X\right\}\right)$$
4		simp3	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge X\in S\wedge Y\in T\right)\to Y\in T$$
5		fsnunf	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge \left(X\in S\wedge \neg X\in \left(S\setminus \left\{X\right\}\right)\right)\wedge Y\in T\right)\to \left(F\cup \left\{⟨X,Y⟩\right\}\right):\left(S\setminus \left\{X\right\}\right)\cup \left\{X\right\}⟶T$$
6	1 2 3 4 5	syl121anc	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge X\in S\wedge Y\in T\right)\to \left(F\cup \left\{⟨X,Y⟩\right\}\right):\left(S\setminus \left\{X\right\}\right)\cup \left\{X\right\}⟶T$$
7		difsnid	$$⊢X\in S\to \left(S\setminus \left\{X\right\}\right)\cup \left\{X\right\}=S$$
8	7	3ad2ant2	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge X\in S\wedge Y\in T\right)\to \left(S\setminus \left\{X\right\}\right)\cup \left\{X\right\}=S$$
9	8	feq2d	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge X\in S\wedge Y\in T\right)\to \left(\left(F\cup \left\{⟨X,Y⟩\right\}\right):\left(S\setminus \left\{X\right\}\right)\cup \left\{X\right\}⟶T\leftrightarrow \left(F\cup \left\{⟨X,Y⟩\right\}\right):S⟶T\right)$$
10	6 9	mpbid	$$⊢\left(F:S\setminus \left\{X\right\}⟶T\wedge X\in S\wedge Y\in T\right)\to \left(F\cup \left\{⟨X,Y⟩\right\}\right):S⟶T$$