Theorem fnunop

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

	Ref	Expression
Hypotheses	fnunop.x	$$⊢\phi \to X\in V$$
	fnunop.y	$$⊢\phi \to Y\in W$$
	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	fnunop	$$⊢\phi \to GFnE$$

Proof

Step	Hyp	Ref	Expression
1		fnunop.x	$$⊢\phi \to X\in V$$
2		fnunop.y	$$⊢\phi \to Y\in W$$
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 V\wedge Y\in W\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	3 8 10	fnund	$$⊢\phi \to \left(F\cup \left\{⟨X,Y⟩\right\}\right)Fn\left(D\cup \left\{X\right\}\right)$$
12	4	fneq1i	$$⊢GFnE\leftrightarrow \left(F\cup \left\{⟨X,Y⟩\right\}\right)FnE$$
13	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)$$
14	12 13	bitri	$$⊢GFnE\leftrightarrow \left(F\cup \left\{⟨X,Y⟩\right\}\right)Fn\left(D\cup \left\{X\right\}\right)$$
15	11 14	sylibr	$$⊢\phi \to GFnE$$