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	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → 𝐹 : 𝐴 –1-1→ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		f1fn	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 Fn 𝐴 )
2	1	adantr	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → 𝐹 Fn 𝐴 )
3		simpr	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → ran 𝐹 ⊆ 𝐶 )
4		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐶 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐶 ) )
5	2 3 4	sylanbrc	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → 𝐹 : 𝐴 ⟶ 𝐶 )
6		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
7	6	simprbi	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun ◡ 𝐹 )
8	7	adantr	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → Fun ◡ 𝐹 )
9		df-f1	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐶 ↔ ( 𝐹 : 𝐴 ⟶ 𝐶 ∧ Fun ◡ 𝐹 ) )
10	5 8 9	sylanbrc	⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ ran 𝐹 ⊆ 𝐶 ) → 𝐹 : 𝐴 –1-1→ 𝐶 )