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

Theorem resfunexg 5698
Description: The restriction of a function to a set exists. Compare Proposition 6.17 of [TakeutiZaring] p. 28. (Contributed by NM, 7-Apr-1995.) (Revised by Mario Carneiro, 22-Jun-2013.)
Assertion
Ref Expression
resfunexg  |-  ( ( Fun  A  /\  B  e.  C )  ->  ( A  |`  B )  e. 
_V )
Dummy variable  x is distinct from all other variables.

Proof of Theorem resfunexg
StepHypRef Expression
1 funres 5258 . . . . . . 7  |-  ( Fun 
A  ->  Fun  ( A  |`  B ) )
21adantr 453 . . . . . 6  |-  ( ( Fun  A  /\  B  e.  C )  ->  Fun  ( A  |`  B ) )
3 funfn 5249 . . . . . 6  |-  ( Fun  ( A  |`  B )  <-> 
( A  |`  B )  Fn  dom  (  A  |`  B ) )
42, 3sylib 190 . . . . 5  |-  ( ( Fun  A  /\  B  e.  C )  ->  ( A  |`  B )  Fn 
dom  (  A  |`  B ) )
5 dffn5 5529 . . . . 5  |-  ( ( A  |`  B )  Fn  dom  (  A  |`  B )  <->  ( A  |`  B )  =  ( x  e.  dom  (  A  |`  B )  |->  ( ( A  |`  B ) `
 x ) ) )
64, 5sylib 190 . . . 4  |-  ( ( Fun  A  /\  B  e.  C )  ->  ( A  |`  B )  =  ( x  e.  dom  (  A  |`  B ) 
|->  ( ( A  |`  B ) `  x
) ) )
7 fvex 5499 . . . . 5  |-  ( ( A  |`  B ) `  x )  e.  _V
87fnasrn 5663 . . . 4  |-  ( x  e.  dom  (  A  |`  B )  |->  ( ( A  |`  B ) `  x ) )  =  ran  (  x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. )
96, 8syl6eq 2332 . . 3  |-  ( ( Fun  A  /\  B  e.  C )  ->  ( A  |`  B )  =  ran  (  x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. ) )
10 opex 4236 . . . . . 6  |-  <. x ,  ( ( A  |`  B ) `  x
) >.  e.  _V
11 eqid 2284 . . . . . 6  |-  ( x  e.  dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. )  =  ( x  e.  dom  (  A  |`  B )  |->  <.
x ,  ( ( A  |`  B ) `  x ) >. )
1210, 11dmmpti 5338 . . . . 5  |-  dom  (  x  e.  dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. )  =  dom  (  A  |`  B )
1312imaeq2i 5009 . . . 4  |-  ( ( x  e.  dom  (  A  |`  B )  |->  <.
x ,  ( ( A  |`  B ) `  x ) >. ) " dom  (  x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. ) )  =  ( ( x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. ) " dom  (  A  |`  B ) )
14 imadmrn 5023 . . . 4  |-  ( ( x  e.  dom  (  A  |`  B )  |->  <.
x ,  ( ( A  |`  B ) `  x ) >. ) " dom  (  x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. ) )  =  ran  (  x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. )
1513, 14eqtr3i 2306 . . 3  |-  ( ( x  e.  dom  (  A  |`  B )  |->  <.
x ,  ( ( A  |`  B ) `  x ) >. ) " dom  (  A  |`  B ) )  =  ran  (  x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. )
169, 15syl6eqr 2334 . 2  |-  ( ( Fun  A  /\  B  e.  C )  ->  ( A  |`  B )  =  ( ( x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. ) " dom  (  A  |`  B ) ) )
17 funmpt 5256 . . 3  |-  Fun  (
x  e.  dom  (  A  |`  B )  |->  <.
x ,  ( ( A  |`  B ) `  x ) >. )
18 dmresexg 4977 . . . 4  |-  ( B  e.  C  ->  dom  (  A  |`  B )  e.  _V )
1918adantl 454 . . 3  |-  ( ( Fun  A  /\  B  e.  C )  ->  dom  (  A  |`  B )  e.  _V )
20 funimaexg 5294 . . 3  |-  ( ( Fun  ( x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. )  /\  dom  (  A  |`  B )  e.  _V )  -> 
( ( x  e. 
dom  (  A  |`  B )  |->  <. x ,  ( ( A  |`  B ) `  x
) >. ) " dom  (  A  |`  B ) )  e.  _V )
2117, 19, 20sylancr 646 . 2  |-  ( ( Fun  A  /\  B  e.  C )  ->  (
( x  e.  dom  (  A  |`  B ) 
|->  <. x ,  ( ( A  |`  B ) `
 x ) >.
) " dom  (  A  |`  B ) )  e.  _V )
2216, 21eqeltrd 2358 1  |-  ( ( Fun  A  /\  B  e.  C )  ->  ( A  |`  B )  e. 
_V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    = wceq 1624    e. wcel 1685   _Vcvv 2789   <.cop 3644    e. cmpt 4078   dom cdm 4688   ran crn 4689    |` cres 4690   "cima 4691   Fun wfun 5215    Fn wfn 5216   ` cfv 5221
This theorem is referenced by:  cofunexg  5700  fnex  5702  ofexg  6043  dfac8alem  7651  dfac12lem1  7764  cfsmolem  7891  alephsing  7897  itunifval  8037  zorn2lem1  8118  ttukeylem3  8133  imadomg  8154  wunex2  8355  inar1  8392  axdc4uzlem  11038  1stf1  13960  1stf2  13961  2ndf1  13963  2ndf2  13964  1stfcl  13965  2ndfcl  13966  bpolylem  24190  valtar  25282  idcatfun  25340  domidmor  25347  codidmor  25349  grphidmor  25351  dnnumch1  26540  aomclem6  26555  tendo02  30243
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-rep 4132  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-reu 2551  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-iun 3908  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-f 5225  df-f1 5226  df-fo 5227  df-f1o 5228  df-fv 5229
  Copyright terms: Public domain W3C validator