Metamath Proof Explorer

Theorem fressnfv

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

Ref Expression
Assertion fressnfv 
|- ( ( F Fn A /\ B e. A ) -> ( ( F |` { B } ) : { B } --> C <-> ( F ` B ) e. C ) )

Proof

Step Hyp Ref Expression
1 sneq 
 |-  ( x = B -> { x } = { B } )
2 reseq2 
 |-  ( { x } = { B } -> ( F |` { x } ) = ( F |` { B } ) )
3 2 feq1d 
 |-  ( { x } = { B } -> ( ( F |` { x } ) : { x } --> C <-> ( F |` { B } ) : { x } --> C ) )
4 feq2 
 |-  ( { x } = { B } -> ( ( F |` { B } ) : { x } --> C <-> ( F |` { B } ) : { B } --> C ) )
5 3 4 bitrd 
 |-  ( { x } = { B } -> ( ( F |` { x } ) : { x } --> C <-> ( F |` { B } ) : { B } --> C ) )
6 1 5 syl 
 |-  ( x = B -> ( ( F |` { x } ) : { x } --> C <-> ( F |` { B } ) : { B } --> C ) )
7 fveq2 
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
8 7 eleq1d 
 |-  ( x = B -> ( ( F ` x ) e. C <-> ( F ` B ) e. C ) )
9 6 8 bibi12d 
 |-  ( x = B -> ( ( ( F |` { x } ) : { x } --> C <-> ( F ` x ) e. C ) <-> ( ( F |` { B } ) : { B } --> C <-> ( F ` B ) e. C ) ) )
10 9 imbi2d 
 |-  ( x = B -> ( ( F Fn A -> ( ( F |` { x } ) : { x } --> C <-> ( F ` x ) e. C ) ) <-> ( F Fn A -> ( ( F |` { B } ) : { B } --> C <-> ( F ` B ) e. C ) ) ) )
11 fnressn 
 |-  ( ( F Fn A /\ x e. A ) -> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
12 vsnid 
 |-  x e. { x }
13 fvres 
 |-  ( x e. { x } -> ( ( F |` { x } ) ` x ) = ( F ` x ) )
14 12 13 ax-mp 
 |-  ( ( F |` { x } ) ` x ) = ( F ` x )
15 14 opeq2i 
 |-  <. x , ( ( F |` { x } ) ` x ) >. = <. x , ( F ` x ) >.
16 15 sneqi 
 |-  { <. x , ( ( F |` { x } ) ` x ) >. } = { <. x , ( F ` x ) >. }
17 16 eqeq2i 
 |-  ( ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } <-> ( F |` { x } ) = { <. x , ( F ` x ) >. } )
18 vex 
 |-  x e. _V
19 18 fsn2 
 |-  ( ( F |` { x } ) : { x } --> C <-> ( ( ( F |` { x } ) ` x ) e. C /\ ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } ) )
20 iba 
 |-  ( ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } -> ( ( ( F |` { x } ) ` x ) e. C <-> ( ( ( F |` { x } ) ` x ) e. C /\ ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } ) ) )
21 14 eleq1i 
 |-  ( ( ( F |` { x } ) ` x ) e. C <-> ( F ` x ) e. C )
22 20 21 bitr3di 
 |-  ( ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } -> ( ( ( ( F |` { x } ) ` x ) e. C /\ ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } ) <-> ( F ` x ) e. C ) )
23 19 22 syl5bb 
 |-  ( ( F |` { x } ) = { <. x , ( ( F |` { x } ) ` x ) >. } -> ( ( F |` { x } ) : { x } --> C <-> ( F ` x ) e. C ) )
24 17 23 sylbir 
 |-  ( ( F |` { x } ) = { <. x , ( F ` x ) >. } -> ( ( F |` { x } ) : { x } --> C <-> ( F ` x ) e. C ) )
25 11 24 syl 
 |-  ( ( F Fn A /\ x e. A ) -> ( ( F |` { x } ) : { x } --> C <-> ( F ` x ) e. C ) )
26 25 expcom 
 |-  ( x e. A -> ( F Fn A -> ( ( F |` { x } ) : { x } --> C <-> ( F ` x ) e. C ) ) )
27 10 26 vtoclga 
 |-  ( B e. A -> ( F Fn A -> ( ( F |` { B } ) : { B } --> C <-> ( F ` B ) e. C ) ) )
28 27 impcom 
 |-  ( ( F Fn A /\ B e. A ) -> ( ( F |` { B } ) : { B } --> C <-> ( F ` B ) e. C ) )