Metamath Proof Explorer

Theorem fsnunf2

Description: Adjoining a point to a punctured function gives a function. (Contributed by Stefan O'Rear, 28-Feb-2015)

Ref Expression
Assertion fsnunf2 
|- ( ( F : ( S \ { X } ) --> T /\ X e. S /\ Y e. T ) -> ( F u. { <. X , Y >. } ) : S --> T )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F : ( S \ { X } ) --> T /\ X e. S /\ Y e. T ) -> F : ( S \ { X } ) --> T )
2 simp2 
 |-  ( ( F : ( S \ { X } ) --> T /\ X e. S /\ Y e. T ) -> X e. S )
3 neldifsnd 
 |-  ( ( F : ( S \ { X } ) --> T /\ X e. S /\ Y e. T ) -> -. X e. ( S \ { X } ) )
4 simp3 
 |-  ( ( F : ( S \ { X } ) --> T /\ X e. S /\ Y e. T ) -> Y e. T )
5 fsnunf 
 |-  ( ( F : ( S \ { X } ) --> T /\ ( X e. S /\ -. X e. ( S \ { X } ) ) /\ Y e. T ) -> ( F u. { <. X , Y >. } ) : ( ( S \ { X } ) u. { X } ) --> T )
6 1 2 3 4 5 syl121anc 
 |-  ( ( F : ( S \ { X } ) --> T /\ X e. S /\ Y e. T ) -> ( F u. { <. X , Y >. } ) : ( ( S \ { X } ) u. { X } ) --> T )
7 difsnid 
 |-  ( X e. S -> ( ( S \ { X } ) u. { X } ) = S )
8 7 3ad2ant2 
 |-  ( ( F : ( S \ { X } ) --> T /\ X e. S /\ Y e. T ) -> ( ( S \ { X } ) u. { X } ) = S )
9 8 feq2d 
 |-  ( ( F : ( S \ { X } ) --> T /\ X e. S /\ Y e. T ) -> ( ( F u. { <. X , Y >. } ) : ( ( S \ { X } ) u. { X } ) --> T <-> ( F u. { <. X , Y >. } ) : S --> T ) )
10 6 9 mpbid 
 |-  ( ( F : ( S \ { X } ) --> T /\ X e. S /\ Y e. T ) -> ( F u. { <. X , Y >. } ) : S --> T )