# Metamath Proof Explorer

## Theorem fores

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

Ref Expression
Assertion fores ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left({{F}↾}_{{A}}\right):{A}\underset{onto}{⟶}{F}\left[{A}\right]$

### Proof

Step Hyp Ref Expression
1 funres ${⊢}\mathrm{Fun}{F}\to \mathrm{Fun}\left({{F}↾}_{{A}}\right)$
2 1 anim1i ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left(\mathrm{Fun}\left({{F}↾}_{{A}}\right)\wedge {A}\subseteq \mathrm{dom}{F}\right)$
3 df-fn ${⊢}\left({{F}↾}_{{A}}\right)Fn{A}↔\left(\mathrm{Fun}\left({{F}↾}_{{A}}\right)\wedge \mathrm{dom}\left({{F}↾}_{{A}}\right)={A}\right)$
4 df-ima ${⊢}{F}\left[{A}\right]=\mathrm{ran}\left({{F}↾}_{{A}}\right)$
5 4 eqcomi ${⊢}\mathrm{ran}\left({{F}↾}_{{A}}\right)={F}\left[{A}\right]$
6 df-fo ${⊢}\left({{F}↾}_{{A}}\right):{A}\underset{onto}{⟶}{F}\left[{A}\right]↔\left(\left({{F}↾}_{{A}}\right)Fn{A}\wedge \mathrm{ran}\left({{F}↾}_{{A}}\right)={F}\left[{A}\right]\right)$
7 5 6 mpbiran2 ${⊢}\left({{F}↾}_{{A}}\right):{A}\underset{onto}{⟶}{F}\left[{A}\right]↔\left({{F}↾}_{{A}}\right)Fn{A}$
8 ssdmres ${⊢}{A}\subseteq \mathrm{dom}{F}↔\mathrm{dom}\left({{F}↾}_{{A}}\right)={A}$
9 8 anbi2i ${⊢}\left(\mathrm{Fun}\left({{F}↾}_{{A}}\right)\wedge {A}\subseteq \mathrm{dom}{F}\right)↔\left(\mathrm{Fun}\left({{F}↾}_{{A}}\right)\wedge \mathrm{dom}\left({{F}↾}_{{A}}\right)={A}\right)$
10 3 7 9 3bitr4i ${⊢}\left({{F}↾}_{{A}}\right):{A}\underset{onto}{⟶}{F}\left[{A}\right]↔\left(\mathrm{Fun}\left({{F}↾}_{{A}}\right)\wedge {A}\subseteq \mathrm{dom}{F}\right)$
11 2 10 sylibr ${⊢}\left(\mathrm{Fun}{F}\wedge {A}\subseteq \mathrm{dom}{F}\right)\to \left({{F}↾}_{{A}}\right):{A}\underset{onto}{⟶}{F}\left[{A}\right]$