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

Metamath Proof Explorer

Theorem fsnunres

Description: Recover the original function from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Assertion fsnunres 
|- ( ( F Fn S /\ -. X e. S ) -> ( ( F u. { <. X , Y >. } ) |` S ) = F )

Proof

Step Hyp Ref Expression
1 fnresdm 
 |-  ( F Fn S -> ( F |` S ) = F )
2 1 adantr 
 |-  ( ( F Fn S /\ -. X e. S ) -> ( F |` S ) = F )
3 ressnop0 
 |-  ( -. X e. S -> ( { <. X , Y >. } |` S ) = (/) )
4 3 adantl 
 |-  ( ( F Fn S /\ -. X e. S ) -> ( { <. X , Y >. } |` S ) = (/) )
5 2 4 uneq12d 
 |-  ( ( F Fn S /\ -. X e. S ) -> ( ( F |` S ) u. ( { <. X , Y >. } |` S ) ) = ( F u. (/) ) )
6 resundir 
 |-  ( ( F u. { <. X , Y >. } ) |` S ) = ( ( F |` S ) u. ( { <. X , Y >. } |` S ) )
7 un0 
 |-  ( F u. (/) ) = F
8 7 eqcomi 
 |-  F = ( F u. (/) )
9 5 6 8 3eqtr4g 
 |-  ( ( F Fn S /\ -. X e. S ) -> ( ( F u. { <. X , Y >. } ) |` S ) = F )