Metamath Proof Explorer

Theorem funressn

Description: A function restricted to a singleton. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion funressn 
|- ( Fun F -> ( F |` { B } ) C_ { <. B , ( F ` B ) >. } )

Proof

Step Hyp Ref Expression
1 funfn 
 |-  ( Fun F <-> F Fn dom F )
2 fnressn 
 |-  ( ( F Fn dom F /\ B e. dom F ) -> ( F |` { B } ) = { <. B , ( F ` B ) >. } )
3 1 2 sylanb 
 |-  ( ( Fun F /\ B e. dom F ) -> ( F |` { B } ) = { <. B , ( F ` B ) >. } )
4 eqimss 
 |-  ( ( F |` { B } ) = { <. B , ( F ` B ) >. } -> ( F |` { B } ) C_ { <. B , ( F ` B ) >. } )
5 3 4 syl 
 |-  ( ( Fun F /\ B e. dom F ) -> ( F |` { B } ) C_ { <. B , ( F ` B ) >. } )
6 disjsn 
 |-  ( ( dom F i^i { B } ) = (/) <-> -. B e. dom F )
7 fnresdisj 
 |-  ( F Fn dom F -> ( ( dom F i^i { B } ) = (/) <-> ( F |` { B } ) = (/) ) )
8 1 7 sylbi 
 |-  ( Fun F -> ( ( dom F i^i { B } ) = (/) <-> ( F |` { B } ) = (/) ) )
9 6 8 bitr3id 
 |-  ( Fun F -> ( -. B e. dom F <-> ( F |` { B } ) = (/) ) )
10 9 biimpa 
 |-  ( ( Fun F /\ -. B e. dom F ) -> ( F |` { B } ) = (/) )
11 0ss 
 |-  (/) C_ { <. B , ( F ` B ) >. }
12 10 11 eqsstrdi 
 |-  ( ( Fun F /\ -. B e. dom F ) -> ( F |` { B } ) C_ { <. B , ( F ` B ) >. } )
13 5 12 pm2.61dan 
 |-  ( Fun F -> ( F |` { B } ) C_ { <. B , ( F ` B ) >. } )