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 )