MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnressn Structured version   Visualization version   Unicode version

Theorem fnressn 6081
Description: A function restricted to a singleton. (Contributed by NM, 9-Oct-2004.)
Assertion
Ref Expression
fnressn  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( F  |`  { B } )  =  { <. B ,  ( F `
 B ) >. } )

Proof of Theorem fnressn
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 sneq 3980 . . . . . 6  |-  ( x  =  B  ->  { x }  =  { B } )
21reseq2d 5108 . . . . 5  |-  ( x  =  B  ->  ( F  |`  { x }
)  =  ( F  |`  { B } ) )
3 fveq2 5870 . . . . . . 7  |-  ( x  =  B  ->  ( F `  x )  =  ( F `  B ) )
4 opeq12 4171 . . . . . . 7  |-  ( ( x  =  B  /\  ( F `  x )  =  ( F `  B ) )  ->  <. x ,  ( F `
 x ) >.  =  <. B ,  ( F `  B )
>. )
53, 4mpdan 675 . . . . . 6  |-  ( x  =  B  ->  <. x ,  ( F `  x ) >.  =  <. B ,  ( F `  B ) >. )
65sneqd 3982 . . . . 5  |-  ( x  =  B  ->  { <. x ,  ( F `  x ) >. }  =  { <. B ,  ( F `  B )
>. } )
72, 6eqeq12d 2468 . . . 4  |-  ( x  =  B  ->  (
( F  |`  { x } )  =  { <. x ,  ( F `
 x ) >. } 
<->  ( F  |`  { B } )  =  { <. B ,  ( F `
 B ) >. } ) )
87imbi2d 318 . . 3  |-  ( x  =  B  ->  (
( F  Fn  A  ->  ( F  |`  { x } )  =  { <. x ,  ( F `
 x ) >. } )  <->  ( F  Fn  A  ->  ( F  |`  { B } )  =  { <. B , 
( F `  B
) >. } ) ) )
9 vex 3050 . . . . . . 7  |-  x  e. 
_V
109snss 4099 . . . . . 6  |-  ( x  e.  A  <->  { x }  C_  A )
11 fnssres 5694 . . . . . 6  |-  ( ( F  Fn  A  /\  { x }  C_  A
)  ->  ( F  |` 
{ x } )  Fn  { x }
)
1210, 11sylan2b 478 . . . . 5  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( F  |`  { x } )  Fn  {
x } )
13 dffn2 5735 . . . . . 6  |-  ( ( F  |`  { x } )  Fn  {
x }  <->  ( F  |` 
{ x } ) : { x } --> _V )
149fsn2 6067 . . . . . 6  |-  ( ( F  |`  { x } ) : {
x } --> _V  <->  ( (
( F  |`  { x } ) `  x
)  e.  _V  /\  ( F  |`  { x } )  =  { <. x ,  ( ( F  |`  { x } ) `  x
) >. } ) )
15 fvex 5880 . . . . . . . 8  |-  ( ( F  |`  { x } ) `  x
)  e.  _V
1615biantrur 509 . . . . . . 7  |-  ( ( F  |`  { x } )  =  { <. x ,  ( ( F  |`  { x } ) `  x
) >. }  <->  ( (
( F  |`  { x } ) `  x
)  e.  _V  /\  ( F  |`  { x } )  =  { <. x ,  ( ( F  |`  { x } ) `  x
) >. } ) )
17 ssnid 3999 . . . . . . . . . . 11  |-  x  e. 
{ x }
18 fvres 5884 . . . . . . . . . . 11  |-  ( x  e.  { x }  ->  ( ( F  |`  { x } ) `
 x )  =  ( F `  x
) )
1917, 18ax-mp 5 . . . . . . . . . 10  |-  ( ( F  |`  { x } ) `  x
)  =  ( F `
 x )
2019opeq2i 4173 . . . . . . . . 9  |-  <. x ,  ( ( F  |`  { x } ) `
 x ) >.  =  <. x ,  ( F `  x )
>.
2120sneqi 3981 . . . . . . . 8  |-  { <. x ,  ( ( F  |`  { x } ) `
 x ) >. }  =  { <. x ,  ( F `  x ) >. }
2221eqeq2i 2465 . . . . . . 7  |-  ( ( F  |`  { x } )  =  { <. x ,  ( ( F  |`  { x } ) `  x
) >. }  <->  ( F  |` 
{ x } )  =  { <. x ,  ( F `  x ) >. } )
2316, 22bitr3i 255 . . . . . 6  |-  ( ( ( ( F  |`  { x } ) `
 x )  e. 
_V  /\  ( F  |` 
{ x } )  =  { <. x ,  ( ( F  |`  { x } ) `
 x ) >. } )  <->  ( F  |` 
{ x } )  =  { <. x ,  ( F `  x ) >. } )
2413, 14, 233bitri 275 . . . . 5  |-  ( ( F  |`  { x } )  Fn  {
x }  <->  ( F  |` 
{ x } )  =  { <. x ,  ( F `  x ) >. } )
2512, 24sylib 200 . . . 4  |-  ( ( F  Fn  A  /\  x  e.  A )  ->  ( F  |`  { x } )  =  { <. x ,  ( F `
 x ) >. } )
2625expcom 437 . . 3  |-  ( x  e.  A  ->  ( F  Fn  A  ->  ( F  |`  { x } )  =  { <. x ,  ( F `
 x ) >. } ) )
278, 26vtoclga 3115 . 2  |-  ( B  e.  A  ->  ( F  Fn  A  ->  ( F  |`  { B } )  =  { <. B ,  ( F `
 B ) >. } ) )
2827impcom 432 1  |-  ( ( F  Fn  A  /\  B  e.  A )  ->  ( F  |`  { B } )  =  { <. B ,  ( F `
 B ) >. } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    = wceq 1446    e. wcel 1889   _Vcvv 3047    C_ wss 3406   {csn 3970   <.cop 3976    |` cres 4839    Fn wfn 5580   -->wf 5581   ` cfv 5585
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-reu 2746  df-rab 2748  df-v 3049  df-sbc 3270  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-id 4752  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5549  df-fun 5587  df-fn 5588  df-f 5589  df-f1 5590  df-fo 5591  df-f1o 5592  df-fv 5593
This theorem is referenced by:  funressn  6082  fressnfv  6083  fnsnsplit  6106  canthp1lem2  9083  fseq1p1m1  11875  dprd2da  17687  dmdprdpr  17694  dprdpr  17695  dpjlem  17696  pgpfaclem1  17726  islindf4  19408  xpstopnlem1  20836  ptcmpfi  20840  2pthlem1  25337  eupath2lem3  25719  ginvsn  26089  subfacp1lem5  29919  cvmliftlem10  30029  poimirlem9  31961  2pthdlem1  39755
  Copyright terms: Public domain W3C validator