# Metamath Proof Explorer

## Theorem f1ssr

Description: A function that is one-to-one is also one-to-one on some superset of its range. (Contributed by Stefan O'Rear, 20-Feb-2015)

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

### Proof

Step Hyp Ref Expression
1 f1fn ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to {F}Fn{A}$
2 1 adantr ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \mathrm{ran}{F}\subseteq {C}\right)\to {F}Fn{A}$
3 simpr ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \mathrm{ran}{F}\subseteq {C}\right)\to \mathrm{ran}{F}\subseteq {C}$
4 df-f ${⊢}{F}:{A}⟶{C}↔\left({F}Fn{A}\wedge \mathrm{ran}{F}\subseteq {C}\right)$
5 2 3 4 sylanbrc ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \mathrm{ran}{F}\subseteq {C}\right)\to {F}:{A}⟶{C}$
6 df-f1 ${⊢}{F}:{A}\underset{1-1}{⟶}{B}↔\left({F}:{A}⟶{B}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
7 6 simprbi ${⊢}{F}:{A}\underset{1-1}{⟶}{B}\to \mathrm{Fun}{{F}}^{-1}$
8 7 adantr ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \mathrm{ran}{F}\subseteq {C}\right)\to \mathrm{Fun}{{F}}^{-1}$
9 df-f1 ${⊢}{F}:{A}\underset{1-1}{⟶}{C}↔\left({F}:{A}⟶{C}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
10 5 8 9 sylanbrc ${⊢}\left({F}:{A}\underset{1-1}{⟶}{B}\wedge \mathrm{ran}{F}\subseteq {C}\right)\to {F}:{A}\underset{1-1}{⟶}{C}$