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 bitrid
 |-  ( ( 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 ) )