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

Metamath Proof Explorer

Theorem fnsnsplit

Description: Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 fnresdm 
 |-  ( F Fn A -> ( F |` A ) = F )
2 1 adantr 
 |-  ( ( F Fn A /\ X e. A ) -> ( F |` A ) = F )
3 resundi 
 |-  ( F |` ( ( A \ { X } ) u. { X } ) ) = ( ( F |` ( A \ { X } ) ) u. ( F |` { X } ) )
4 difsnid 
 |-  ( X e. A -> ( ( A \ { X } ) u. { X } ) = A )
5 4 adantl 
 |-  ( ( F Fn A /\ X e. A ) -> ( ( A \ { X } ) u. { X } ) = A )
6 5 reseq2d 
 |-  ( ( F Fn A /\ X e. A ) -> ( F |` ( ( A \ { X } ) u. { X } ) ) = ( F |` A ) )
7 fnressn 
 |-  ( ( F Fn A /\ X e. A ) -> ( F |` { X } ) = { <. X , ( F ` X ) >. } )
8 7 uneq2d 
 |-  ( ( F Fn A /\ X e. A ) -> ( ( F |` ( A \ { X } ) ) u. ( F |` { X } ) ) = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
9 3 6 8 3eqtr3a 
 |-  ( ( F Fn A /\ X e. A ) -> ( F |` A ) = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
10 2 9 eqtr3d 
 |-  ( ( F Fn A /\ X e. A ) -> F = ( ( F |` ( A \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )