Theorem fnunsn

Description: Extension of a function with a new ordered pair. (Contributed by NM, 28-Sep-2013) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Hypotheses	fnunop.x	$$⊢\phi \to X\in \mathrm{V}$$
	fnunop.y	$$⊢\phi \to Y\in \mathrm{V}$$
	fnunop.f	$$⊢\phi \to FFnD$$
	fnunop.g	$$⊢G=F\cup \left\{⟨X,Y⟩\right\}$$
	fnunop.e	$$⊢E=D\cup \left\{X\right\}$$
	fnunop.d	$$⊢\phi \to \neg X\in D$$
Assertion	fnunsn	$$⊢\phi \to GFnE$$

Proof

Step	Hyp	Ref	Expression
1		fnunop.x	$$⊢\phi \to X\in \mathrm{V}$$
2		fnunop.y	$$⊢\phi \to Y\in \mathrm{V}$$
3		fnunop.f	$$⊢\phi \to FFnD$$
4		fnunop.g	$$⊢G=F\cup \left\{⟨X,Y⟩\right\}$$
5		fnunop.e	$$⊢E=D\cup \left\{X\right\}$$
6		fnunop.d	$$⊢\phi \to \neg X\in D$$
7		fnsng	$$⊢\left(X\in \mathrm{V}\wedge Y\in \mathrm{V}\right)\to \left\{⟨X,Y⟩\right\}Fn\left\{X\right\}$$
8	1 2 7	syl2anc	$$⊢\phi \to \left\{⟨X,Y⟩\right\}Fn\left\{X\right\}$$
9		disjsn	$$⊢D\cap \left\{X\right\}=\varnothing \leftrightarrow \neg X\in D$$
10	6 9	sylibr	$$⊢\phi \to D\cap \left\{X\right\}=\varnothing$$
11		fnun	$$⊢\left(\left(FFnD\wedge \left\{⟨X,Y⟩\right\}Fn\left\{X\right\}\right)\wedge D\cap \left\{X\right\}=\varnothing \right)\to \left(F\cup \left\{⟨X,Y⟩\right\}\right)Fn\left(D\cup \left\{X\right\}\right)$$
12	3 8 10 11	syl21anc	$$⊢\phi \to \left(F\cup \left\{⟨X,Y⟩\right\}\right)Fn\left(D\cup \left\{X\right\}\right)$$
13	4	fneq1i	$$⊢GFnE\leftrightarrow \left(F\cup \left\{⟨X,Y⟩\right\}\right)FnE$$
14	5	fneq2i	$$⊢\left(F\cup \left\{⟨X,Y⟩\right\}\right)FnE\leftrightarrow \left(F\cup \left\{⟨X,Y⟩\right\}\right)Fn\left(D\cup \left\{X\right\}\right)$$
15	13 14	bitri	$$⊢GFnE\leftrightarrow \left(F\cup \left\{⟨X,Y⟩\right\}\right)Fn\left(D\cup \left\{X\right\}\right)$$
16	12 15	sylibr	$$⊢\phi \to GFnE$$