Metamath Proof Explorer

Theorem fnressn

Description: A function restricted to a singleton. (Contributed by NM, 9-Oct-2004)

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

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( x = B -> { x } = { B } )
2 1 reseq2d 
 |-  ( x = B -> ( F |` { x } ) = ( F |` { B } ) )
3 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
4 opeq12 
 |-  ( ( x = B /\ ( F ` x ) = ( F ` B ) ) -> <. x , ( F ` x ) >. = <. B , ( F ` B ) >. )
5 3 4 mpdan 
 |-  ( x = B -> <. x , ( F ` x ) >. = <. B , ( F ` B ) >. )
6 5 sneqd 
 |-  ( x = B -> { <. x , ( F ` x ) >. } = { <. B , ( F ` B ) >. } )
7 2 6 eqeq12d 
 |-  ( x = B -> ( ( F |` { x } ) = { <. x , ( F ` x ) >. } <-> ( F |` { B } ) = { <. B , ( F ` B ) >. } ) )
8 7 imbi2d 
 |-  ( x = B -> ( ( F Fn A -> ( F |` { x } ) = { <. x , ( F ` x ) >. } ) <-> ( F Fn A -> ( F |` { B } ) = { <. B , ( F ` B ) >. } ) ) )
9 vex 
 |-  x e. _V
10 9 snss 
 |-  ( x e. A <-> { x } C_ A )
11 fnssres 
 |-  ( ( F Fn A /\ { x } C_ A ) -> ( F |` { x } ) Fn { x } )
12 10 11 sylan2b 
 |-  ( ( F Fn A /\ x e. A ) -> ( F |` { x } ) Fn { x } )
13 dffn2 
 |-  ( ( F |` { x } ) Fn { x } <-> ( F |` { x } ) : { x } --> _V )
14 9 fsn2 
 |-  ( ( F |` { x } ) : { x } --> _V <-> ( ( ( F |` { x } ) ` x ) e. _V /\ ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } ) )
15 fvex 
 |-  ( ( F |` { x } ) ` x ) e. _V
16 15 biantrur 
 |-  ( ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } <-> ( ( ( F |` { x } ) ` x ) e. _V /\ ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } ) )
17 vsnid 
 |-  x e. { x }
18 fvres 
 |-  ( x e. { x } -> ( ( F |` { x } ) ` x ) = ( F ` x ) )
19 17 18 ax-mp 
 |-  ( ( F |` { x } ) ` x ) = ( F ` x )
20 19 opeq2i 
 |-  <. x , ( ( F |` { x } ) ` x ) >. = <. x , ( F ` x ) >.
21 20 sneqi 
 |-  { <. x , ( ( F |` { x } ) ` x ) >. } = { <. x , ( F ` x ) >. }
22 21 eqeq2i 
 |-  ( ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } <-> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
23 16 22 bitr3i 
 |-  ( ( ( ( F |` { x } ) ` x ) e. _V /\ ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } ) <-> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
24 13 14 23 3bitri 
 |-  ( ( F |` { x } ) Fn { x } <-> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
25 12 24 sylib 
 |-  ( ( F Fn A /\ x e. A ) -> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
26 25 expcom 
 |-  ( x e. A -> ( F Fn A -> ( F |` { x } ) = { <. x , ( F ` x ) >. } ) )
27 8 26 vtoclga 
 |-  ( B e. A -> ( F Fn A -> ( F |` { B } ) = { <. B , ( F ` B ) >. } ) )
28 27 impcom 
 |-  ( ( F Fn A /\ B e. A ) -> ( F |` { B } ) = { <. B , ( F ` B ) >. } )