Theorem fores 5825

Description: Restriction of an onto function. (Contributed by NM, 4-Mar-1997.)

Assertion

Ref	Expression
fores	|- ( ( Fun F /\ A C_ dom F ) -> ( F |` A ) : A -onto-> ( F " A ) )

Proof of Theorem fores

Step	Hyp	Ref	Expression
1		funres 5640	. . 3 |- ( Fun F -> Fun ( F |` A ) )
2	1	anim1i 576	. 2 |- ( ( Fun F /\ A C_ dom F ) -> ( Fun ( F |` A ) /\ A C_ dom F ) )
3		df-fn 5604	. . 3 |- ( ( F |` A ) Fn A <-> ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) )
4		df-ima 4866	. . . . 5 |- ( F " A ) = ran ( F |` A )
5	4	eqcomi 2471	. . . 4 |- ran ( F |` A ) = ( F " A )
6		df-fo 5607	. . . 4 |- ( ( F |` A ) : A -onto-> ( F " A ) <-> ( ( F |` A ) Fn A /\ ran ( F |` A ) = ( F " A ) ) )
7	5, 6	mpbiran2 935	. . 3 |- ( ( F |` A ) : A -onto-> ( F " A ) <-> ( F |` A ) Fn A )
8		ssdmres 5145	. . . 4 |- ( A C_ dom F <-> dom ( F |` A ) = A )
9	8	anbi2i 705	. . 3 |- ( ( Fun ( F |` A ) /\ A C_ dom F ) <-> ( Fun ( F |` A ) /\ dom ( F |` A ) = A ) )
10	3, 7, 9	3bitr4i 285	. 2 |- ( ( F |` A ) : A -onto-> ( F " A ) <-> ( Fun ( F |` A ) /\ A C_ dom F ) )
11	2, 10	sylibr 217	1 |- ( ( Fun F /\ A C_ dom F ) -> ( F |` A ) : A -onto-> ( F " A ) )

Syntax hints:   -> wi 4   /\ wa 375   = wceq 1455   C_ wss 3416   dom cdm 4853   ran crn 4854   |` cres 4855   "cima 4856   Fun wfun 5595   Fn wfn 5596   -onto->wfo 5599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-res 4865  df-ima 4866  df-fun 5603  df-fn 5604  df-fo 5607

This theorem is referenced by:  resdif  5857  f1oweALT  6804  imafi  7893  f1opwfi  7904  fodomfi2  8517  fin1a2lem7  8862  znnen  14314  conima  20489  1stcfb  20509  1stckgenlem  20617  qtoprest  20781  re2ndc  21868  uniiccdif  22584  opnmblALT  22610  mbfimaopnlem  22660  ghsubgolemOLD  26147  ffsrn  28363  erdszelem2  29964  ivthALT  31040  poimirlem26  32011  poimirlem27  32012  lmhmfgima  35987