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

Metamath Proof Explorer

Theorem funresdfunsn

Description: Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself. (Contributed by AV, 2-Dec-2018)

Ref Expression
Assertion funresdfunsn 
|- ( ( Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = F )

Proof

Step Hyp Ref Expression
1 funrel 
 |-  ( Fun F -> Rel F )
2 resdmdfsn 
 |-  ( Rel F -> ( F |` ( _V \ { X } ) ) = ( F |` ( dom F \ { X } ) ) )
3 1 2 syl 
 |-  ( Fun F -> ( F |` ( _V \ { X } ) ) = ( F |` ( dom F \ { X } ) ) )
4 3 adantr 
 |-  ( ( Fun F /\ X e. dom F ) -> ( F |` ( _V \ { X } ) ) = ( F |` ( dom F \ { X } ) ) )
5 4 uneq1d 
 |-  ( ( Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = ( ( F |` ( dom F \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
6 funfn 
 |-  ( Fun F <-> F Fn dom F )
7 fnsnsplit 
 |-  ( ( F Fn dom F /\ X e. dom F ) -> F = ( ( F |` ( dom F \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
8 6 7 sylanb 
 |-  ( ( Fun F /\ X e. dom F ) -> F = ( ( F |` ( dom F \ { X } ) ) u. { <. X , ( F ` X ) >. } ) )
9 5 8 eqtr4d 
 |-  ( ( Fun F /\ X e. dom F ) -> ( ( F |` ( _V \ { X } ) ) u. { <. X , ( F ` X ) >. } ) = F )