fsnunfv

Description: Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by NM, 18-May-2017)

		Ref	Expression
	Assertion	fsnunfv	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to (F \cup \{⟨X, Y⟩\}) (X) = Y$

Proof

Step	Hyp	Ref	Expression
1		dmres	$⊢ dom ({F ↾}_{\{X\}}) = \{X\} \cap dom F$
2		incom	$⊢ \{X\} \cap dom F = dom F \cap \{X\}$
3	1 2	eqtri	$⊢ dom ({F ↾}_{\{X\}}) = dom F \cap \{X\}$
4		disjsn	$⊢ dom F \cap \{X\} = \emptyset \leftrightarrow \neg X \in dom F$
5	4	biimpri	$⊢ \neg X \in dom F \to dom F \cap \{X\} = \emptyset$
6	3 5	eqtrid	$⊢ \neg X \in dom F \to dom ({F ↾}_{\{X\}}) = \emptyset$
7	6	3ad2ant3	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to dom ({F ↾}_{\{X\}}) = \emptyset$
8		relres	$⊢ Rel ({F ↾}_{\{X\}})$
9		reldm0	$⊢ Rel ({F ↾}_{\{X\}}) \to ({F ↾}_{\{X\}} = \emptyset \leftrightarrow dom ({F ↾}_{\{X\}}) = \emptyset)$
10	8 9	ax-mp	$⊢ {F ↾}_{\{X\}} = \emptyset \leftrightarrow dom ({F ↾}_{\{X\}}) = \emptyset$
11	7 10	sylibr	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to {F ↾}_{\{X\}} = \emptyset$
12		fnsng	$⊢ (X \in V \land Y \in W) \to \{⟨X, Y⟩\} Fn \{X\}$
13	12	3adant3	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to \{⟨X, Y⟩\} Fn \{X\}$
14		fnresdm	$⊢ \{⟨X, Y⟩\} Fn \{X\} \to {\{⟨X, Y⟩\} ↾}_{\{X\}} = \{⟨X, Y⟩\}$
15	13 14	syl	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to {\{⟨X, Y⟩\} ↾}_{\{X\}} = \{⟨X, Y⟩\}$
16	11 15	uneq12d	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to ({F ↾}_{\{X\}}) \cup ({\{⟨X, Y⟩\} ↾}_{\{X\}}) = \emptyset \cup \{⟨X, Y⟩\}$
17		resundir	$⊢ {(F \cup \{⟨X, Y⟩\}) ↾}_{\{X\}} = ({F ↾}_{\{X\}}) \cup ({\{⟨X, Y⟩\} ↾}_{\{X\}})$
18		uncom	$⊢ \emptyset \cup \{⟨X, Y⟩\} = \{⟨X, Y⟩\} \cup \emptyset$
19		un0	$⊢ \{⟨X, Y⟩\} \cup \emptyset = \{⟨X, Y⟩\}$
20	18 19	eqtr2i	$⊢ \{⟨X, Y⟩\} = \emptyset \cup \{⟨X, Y⟩\}$
21	16 17 20	3eqtr4g	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to {(F \cup \{⟨X, Y⟩\}) ↾}_{\{X\}} = \{⟨X, Y⟩\}$
22	21	fveq1d	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to ({(F \cup \{⟨X, Y⟩\}) ↾}_{\{X\}}) (X) = \{⟨X, Y⟩\} (X)$
23		snidg	$⊢ X \in V \to X \in \{X\}$
24	23	3ad2ant1	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to X \in \{X\}$
25	24	fvresd	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to ({(F \cup \{⟨X, Y⟩\}) ↾}_{\{X\}}) (X) = (F \cup \{⟨X, Y⟩\}) (X)$
26		fvsng	$⊢ (X \in V \land Y \in W) \to \{⟨X, Y⟩\} (X) = Y$
27	26	3adant3	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to \{⟨X, Y⟩\} (X) = Y$
28	22 25 27	3eqtr3d	$⊢ (X \in V \land Y \in W \land \neg X \in dom F) \to (F \cup \{⟨X, Y⟩\}) (X) = Y$

Metamath Proof Explorer

Theorem fsnunfv

Proof