Metamath Proof Explorer

Theorem fsnunfv

Description: Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by NM, 18-May-2017)

Ref Expression
Assertion fsnunfv 
|- ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> ( ( F u. { <. X , Y >. } ) ` X ) = Y )

Proof

Step Hyp Ref Expression
1 dmres 
 |-  dom ( F |` { X } ) = ( { X } i^i dom F )
2 incom 
 |-  ( { X } i^i dom F ) = ( dom F i^i { X } )
3 1 2 eqtri 
 |-  dom ( F |` { X } ) = ( dom F i^i { X } )
4 disjsn 
 |-  ( ( dom F i^i { X } ) = (/) <-> -. X e. dom F )
5 4 biimpri 
 |-  ( -. X e. dom F -> ( dom F i^i { X } ) = (/) )
6 3 5 eqtrid 
 |-  ( -. X e. dom F -> dom ( F |` { X } ) = (/) )
7 6 3ad2ant3 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> dom ( F |` { X } ) = (/) )
8 relres 
 |-  Rel ( F |` { X } )
9 reldm0 
 |-  ( Rel ( F |` { X } ) -> ( ( F |` { X } ) = (/) <-> dom ( F |` { X } ) = (/) ) )
10 8 9 ax-mp 
 |-  ( ( F |` { X } ) = (/) <-> dom ( F |` { X } ) = (/) )
11 7 10 sylibr 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> ( F |` { X } ) = (/) )
12 fnsng 
 |-  ( ( X e. V /\ Y e. W ) -> { <. X , Y >. } Fn { X } )
13 12 3adant3 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> { <. X , Y >. } Fn { X } )
14 fnresdm 
 |-  ( { <. X , Y >. } Fn { X } -> ( { <. X , Y >. } |` { X } ) = { <. X , Y >. } )
15 13 14 syl 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> ( { <. X , Y >. } |` { X } ) = { <. X , Y >. } )
16 11 15 uneq12d 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> ( ( F |` { X } ) u. ( { <. X , Y >. } |` { X } ) ) = ( (/) u. { <. X , Y >. } ) )
17 resundir 
 |-  ( ( F u. { <. X , Y >. } ) |` { X } ) = ( ( F |` { X } ) u. ( { <. X , Y >. } |` { X } ) )
18 uncom 
 |-  ( (/) u. { <. X , Y >. } ) = ( { <. X , Y >. } u. (/) )
19 un0 
 |-  ( { <. X , Y >. } u. (/) ) = { <. X , Y >. }
20 18 19 eqtr2i 
 |-  { <. X , Y >. } = ( (/) u. { <. X , Y >. } )
21 16 17 20 3eqtr4g 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> ( ( F u. { <. X , Y >. } ) |` { X } ) = { <. X , Y >. } )
22 21 fveq1d 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> ( ( ( F u. { <. X , Y >. } ) |` { X } ) ` X ) = ( { <. X , Y >. } ` X ) )
23 snidg 
 |-  ( X e. V -> X e. { X } )
24 23 3ad2ant1 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> X e. { X } )
25 24 fvresd 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> ( ( ( F u. { <. X , Y >. } ) |` { X } ) ` X ) = ( ( F u. { <. X , Y >. } ) ` X ) )
26 fvsng 
 |-  ( ( X e. V /\ Y e. W ) -> ( { <. X , Y >. } ` X ) = Y )
27 26 3adant3 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> ( { <. X , Y >. } ` X ) = Y )
28 22 25 27 3eqtr3d 
 |-  ( ( X e. V /\ Y e. W /\ -. X e. dom F ) -> ( ( F u. { <. X , Y >. } ) ` X ) = Y )