Metamath Proof Explorer

Theorem fresunsn

Description: Recover the original function from a point-added function. See also funresdfunsn and fsnunres . (Contributed by Thierry Arnoux, 15-Feb-2026)

		Ref	Expression
	Assertion	fresunsn	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to ({F ↾}_{(A ∖ \{X\})}) \cup \{⟨X, Y⟩\} = F$

Proof

Step	Hyp	Ref	Expression
1		resdmdfsn	$⊢ {F ↾}_{(V ∖ \{X\})} = {F ↾}_{(dom F ∖ \{X\})}$
2		fndm	$⊢ F Fn A \to dom F = A$
3	2	3ad2ant1	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to dom F = A$
4	3	difeq1d	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to dom F ∖ \{X\} = A ∖ \{X\}$
5	4	reseq2d	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to {F ↾}_{(dom F ∖ \{X\})} = {F ↾}_{(A ∖ \{X\})}$
6	1 5	eqtr2id	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to {F ↾}_{(A ∖ \{X\})} = {F ↾}_{(V ∖ \{X\})}$
7		simp3	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to F (X) = Y$
8	7	eqcomd	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to Y = F (X)$
9	8	opeq2d	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to ⟨X, Y⟩ = ⟨X, F (X)⟩$
10	9	sneqd	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to \{⟨X, Y⟩\} = \{⟨X, F (X)⟩\}$
11	6 10	uneq12d	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to ({F ↾}_{(A ∖ \{X\})}) \cup \{⟨X, Y⟩\} = ({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, F (X)⟩\}$
12		fnfun	$⊢ F Fn A \to Fun F$
13	12	3ad2ant1	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to Fun F$
14	2	eleq2d	$⊢ F Fn A \to (X \in dom F \leftrightarrow X \in A)$
15	14	biimpar	$⊢ (F Fn A \land X \in A) \to X \in dom F$
16	15	3adant3	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to X \in dom F$
17		funresdfunsn	$⊢ (Fun F \land X \in dom F) \to ({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, F (X)⟩\} = F$
18	13 16 17	syl2anc	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to ({F ↾}_{(V ∖ \{X\})}) \cup \{⟨X, F (X)⟩\} = F$
19	11 18	eqtrd	$⊢ (F Fn A \land X \in A \land F (X) = Y) \to ({F ↾}_{(A ∖ \{X\})}) \cup \{⟨X, Y⟩\} = F$