Theorem f1ss

Description: A function that is one-to-one is also one-to-one on some superset of its codomain. (Contributed by Mario Carneiro, 12-Jan-2013)

	Ref	Expression
Assertion	f1ss	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge B\subseteq C\right)\to F:A\underset{1-1}{⟶}C$$

Proof

Step	Hyp	Ref	Expression
1		f1f	$$⊢F:A\underset{1-1}{⟶}B\to F:A⟶B$$
2		fss	$$⊢\left(F:A⟶B\wedge B\subseteq C\right)\to F:A⟶C$$
3	1 2	sylan	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge B\subseteq C\right)\to F:A⟶C$$
4		df-f1	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \mathrm{Fun}{F}^{-1}\right)$$
5	4	simprbi	$$⊢F:A\underset{1-1}{⟶}B\to \mathrm{Fun}{F}^{-1}$$
6	5	adantr	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge B\subseteq C\right)\to \mathrm{Fun}{F}^{-1}$$
7		df-f1	$$⊢F:A\underset{1-1}{⟶}C\leftrightarrow \left(F:A⟶C\wedge \mathrm{Fun}{F}^{-1}\right)$$
8	3 6 7	sylanbrc	$$⊢\left(F:A\underset{1-1}{⟶}B\wedge B\subseteq C\right)\to F:A\underset{1-1}{⟶}C$$