Theorem f1ores

Description: The restriction of a one-to-one function maps one-to-one onto the image. (Contributed by NM, 25-Mar-1998)

	Ref	Expression
Assertion	f1ores	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]$$

Proof

Step	Hyp	Ref	Expression
1		f1ssres	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C\underset{1-1}{⟶}B$$
2		f1f1orn	$$⊢\left({F\upharpoonright }_C\right):C\underset{1-1}{⟶}B\to \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_C\right)$$
3	1 2	syl	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_C\right)$$
4		df-ima	$$⊢F\left[C\right]=\mathrm{ran}\left({F\upharpoonright }_C\right)$$
5		f1oeq3	$$⊢F\left[C\right]=\mathrm{ran}\left({F\upharpoonright }_C\right)\to \left(\left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]\leftrightarrow \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_C\right)\right)$$
6	4 5	ax-mp	$$⊢\left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]\leftrightarrow \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}\mathrm{ran}\left({F\upharpoonright }_C\right)$$
7	3 6	sylibr	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge C\subseteq A\right)\to \left({F\upharpoonright }_C\right):C\underset{1-1\; onto}{⟶}F\left[C\right]$$