This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐹 : 𝐴 –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→ 𝐶 )