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 /\ X e. A /\ ( F ` X ) = Y ) -> ( ( F |` ( A \ { X } ) ) u. { <. X , Y >. } ) = F )

Proof

Step	Hyp	Ref	Expression
1		resdmdfsn	|- ( F |` ( _V \ { X } ) ) = ( F |` ( dom F \ { X } ) )
2		fndm	|- ( F Fn A -> dom F = A )
3	2	3ad2ant1	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> dom F = A )
4	3	difeq1d	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> ( dom F \ { X } ) = ( A \ { X } ) )
5	4	reseq2d	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> ( F |` ( dom F \ { X } ) ) = ( F |` ( A \ { X } ) ) )
6	1 5	eqtr2id	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> ( F |` ( A \ { X } ) ) = ( F |` ( _V \ { X } ) ) )
7		simp3	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> ( F ` X ) = Y )
8	7	eqcomd	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> Y = ( F ` X ) )
9	8	opeq2d	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> <. X , Y >. = <. X , ( F ` X ) >. )
10	9	sneqd	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> { <. X , Y >. } = { <. X , ( F ` X ) >. } )
11	6 10	uneq12d	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> ( ( F |` ( A \ { X } ) ) u. { <. X , Y >. } ) = ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
12		fnfun	|- ( F Fn A -> Fun F )
13	12	3ad2ant1	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> Fun F )
14	2	eleq2d	|- ( F Fn A -> ( X e. dom F <-> X e. A ) )
15	14	biimpar	|- ( ( F Fn A /\ X e. A ) -> X e. dom F )
16	15	3adant3	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> X e. dom F )
17		funresdfunsn	|- ( ( Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = F )
18	13 16 17	syl2anc	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = F )
19	11 18	eqtrd	|- ( ( F Fn A /\ X e. A /\ ( F ` X ) = Y ) -> ( ( F |` ( A \ { X } ) ) u. { <. X , Y >. } ) = F )