This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ φ \to X \in V$
		fnunop.y	$⊢ φ \to Y \in W$
		fnunop.f	$⊢ φ \to F Fn D$
		fnunop.g	$⊢ G = F \cup \{⟨X, Y⟩\}$
		fnunop.e	$⊢ E = D \cup \{X\}$
		fnunop.d	$⊢ φ \to \neg X \in D$
	Assertion	fnunop	$⊢ φ \to G Fn E$

Proof

Step	Hyp	Ref	Expression
1		fnunop.x	$⊢ φ \to X \in V$
2		fnunop.y	$⊢ φ \to Y \in W$
3		fnunop.f	$⊢ φ \to F Fn D$
4		fnunop.g	$⊢ G = F \cup \{⟨X, Y⟩\}$
5		fnunop.e	$⊢ E = D \cup \{X\}$
6		fnunop.d	$⊢ φ \to \neg X \in D$
7		fnsng	$⊢ (X \in V \land Y \in W) \to \{⟨X, Y⟩\} Fn \{X\}$
8	1 2 7	syl2anc	$⊢ φ \to \{⟨X, Y⟩\} Fn \{X\}$
9		disjsn	$⊢ D \cap \{X\} = \emptyset \leftrightarrow \neg X \in D$
10	6 9	sylibr	$⊢ φ \to D \cap \{X\} = \emptyset$
11	3 8 10	fnund	$⊢ φ \to (F \cup \{⟨X, Y⟩\}) Fn (D \cup \{X\})$
12	4	fneq1i	$⊢ G Fn E \leftrightarrow (F \cup \{⟨X, Y⟩\}) Fn E$
13	5	fneq2i	$⊢ (F \cup \{⟨X, Y⟩\}) Fn E \leftrightarrow (F \cup \{⟨X, Y⟩\}) Fn (D \cup \{X\})$
14	12 13	bitri	$⊢ G Fn E \leftrightarrow (F \cup \{⟨X, Y⟩\}) Fn (D \cup \{X\})$
15	11 14	sylibr	$⊢ φ \to G Fn E$