Theorem fores 6800

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

Assertion

Ref	Expression
fores	⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴))

Proof of Theorem fores

Step	Hyp	Ref	Expression
1		funres 6576	. . 3 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))
2	1	anim1i 626	. 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹))
3		df-fn 6537	. . 3 ⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴))
4		df-ima 5672	. . . . 5 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴)
5	4	eqcomi 2778	. . . 4 ⊢ ran (𝐹 ↾ 𝐴) = (𝐹 “ 𝐴)
6		df-fo 6540	. . . 4 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ ((𝐹 ↾ 𝐴) Fn 𝐴 ∧ ran (𝐹 ↾ 𝐴) = (𝐹 “ 𝐴)))
7	5, 6	mpbiran2 722	. . 3 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (𝐹 ↾ 𝐴) Fn 𝐴)
8		ssdmres 6010	. . . 4 ⊢ (𝐴 ⊆ dom 𝐹 ↔ dom (𝐹 ↾ 𝐴) = 𝐴)
9	8	anbi2i 634	. . 3 ⊢ ((Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴))
10	3, 7, 9	3bitr4i 306	. 2 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹))
11	2, 10	sylibr 237	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567   ⊆ wss 3913  dom cdm 5659  ran crn 5660   ↾ cres 5661   “ cima 5662  Fun wfun 6528   Fn wfn 6529  –onto→wfo 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-res 5671  df-ima 5672  df-fun 6536  df-fn 6537  df-fo 6540

This theorem is referenced by:  fimadmfoALT  6801  resdif  6840  f1oweALT  7965  imafi  9271  f1opwfi  9309  fodomfi2  10040  fin1a2lem7  10386  znnen  16264  connima  23547  1stcfb  23567  1stckgenlem  23675  qtoprest  23839  re2ndc  24923  uniiccdif  25702  opnmblALT  25727  mbfimaopnlem  25779  ffsrn  33010  cycpmconjvlem  33398  erdszelem2  35579  ivthALT  36731  poimirlem26  38180  poimirlem27  38181  lmhmfgima  43698