Theorem fores 6797

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 6575	. . 3 ⊢ (Fun 𝐹 → Fun (𝐹 ↾ 𝐴))
2	1	anim1i 615	. 2 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹))
3		df-fn 6531	. . 3 ⊢ ((𝐹 ↾ 𝐴) Fn 𝐴 ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴))
4		df-ima 5665	. . . . 5 ⊢ (𝐹 “ 𝐴) = ran (𝐹 ↾ 𝐴)
5	4	eqcomi 2743	. . . 4 ⊢ ran (𝐹 ↾ 𝐴) = (𝐹 “ 𝐴)
6		df-fo 6534	. . . 4 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ ((𝐹 ↾ 𝐴) Fn 𝐴 ∧ ran (𝐹 ↾ 𝐴) = (𝐹 “ 𝐴)))
7	5, 6	mpbiran2 710	. . 3 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (𝐹 ↾ 𝐴) Fn 𝐴)
8		ssdmres 5998	. . . 4 ⊢ (𝐴 ⊆ dom 𝐹 ↔ dom (𝐹 ↾ 𝐴) = 𝐴)
9	8	anbi2i 623	. . 3 ⊢ ((Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹) ↔ (Fun (𝐹 ↾ 𝐴) ∧ dom (𝐹 ↾ 𝐴) = 𝐴))
10	3, 7, 9	3bitr4i 303	. 2 ⊢ ((𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴) ↔ (Fun (𝐹 ↾ 𝐴) ∧ 𝐴 ⊆ dom 𝐹))
11	2, 10	sylibr 234	1 ⊢ ((Fun 𝐹 ∧ 𝐴 ⊆ dom 𝐹) → (𝐹 ↾ 𝐴):𝐴–onto→(𝐹 “ 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ⊆ wss 3924  dom cdm 5652  ran crn 5653   ↾ cres 5654   “ cima 5655  Fun wfun 6522   Fn wfn 6523  –onto→wfo 6526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pr 5400

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-br 5118  df-opab 5180  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-res 5664  df-ima 5665  df-fun 6530  df-fn 6531  df-fo 6534

This theorem is referenced by:  fimadmfoALT  6798  resdif  6836  f1oweALT  7966  imafi  9320  f1opwfi  9363  fodomfi2  10067  fin1a2lem7  10413  znnen  16217  connima  23350  1stcfb  23370  1stckgenlem  23478  qtoprest  23642  re2ndc  24727  uniiccdif  25518  opnmblALT  25543  mbfimaopnlem  25595  ffsrn  32642  cycpmconjvlem  33089  erdszelem2  35143  ivthALT  36282  poimirlem26  37599  poimirlem27  37600  lmhmfgima  43040