Metamath Proof Explorer

Theorem fsnunf

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

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> F : S --> T )
2 simp2l 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> X e. V )
3 simp3 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> Y e. T )
4 f1osng 
 |-  ( ( X e. V /\ Y e. T ) -> { <. X , Y >. } : { X } -1-1-onto-> { Y } )
5 2 3 4 syl2anc 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> { <. X , Y >. } : { X } -1-1-onto-> { Y } )
6 f1of 
 |-  ( { <. X , Y >. } : { X } -1-1-onto-> { Y } -> { <. X , Y >. } : { X } --> { Y } )
7 5 6 syl 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> { <. X , Y >. } : { X } --> { Y } )
8 simp2r 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> -. X e. S )
9 disjsn 
 |-  ( ( S i^i { X } ) = (/) <-> -. X e. S )
10 8 9 sylibr 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> ( S i^i { X } ) = (/) )
11 fun 
 |-  ( ( ( F : S --> T /\ { <. X , Y >. } : { X } --> { Y } ) /\ ( S i^i { X } ) = (/) ) -> ( F u. { <. X , Y >. } ) : ( S u. { X } ) --> ( T u. { Y } ) )
12 1 7 10 11 syl21anc 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> ( F u. { <. X , Y >. } ) : ( S u. { X } ) --> ( T u. { Y } ) )
13 snssi 
 |-  ( Y e. T -> { Y } C_ T )
14 13 3ad2ant3 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> { Y } C_ T )
15 ssequn2 
 |-  ( { Y } C_ T <-> ( T u. { Y } ) = T )
16 14 15 sylib 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> ( T u. { Y } ) = T )
17 16 feq3d 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> ( ( F u. { <. X , Y >. } ) : ( S u. { X } ) --> ( T u. { Y } ) <-> ( F u. { <. X , Y >. } ) : ( S u. { X } ) --> T ) )
18 12 17 mpbid 
 |-  ( ( F : S --> T /\ ( X e. V /\ -. X e. S ) /\ Y e. T ) -> ( F u. { <. X , Y >. } ) : ( S u. { X } ) --> T )