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

Proof

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