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

Metamath Proof Explorer

Theorem f1ssres

Description: A function that is one-to-one is also one-to-one on any subclass of its domain. (Contributed by Mario Carneiro, 17-Jan-2015)

Ref Expression
Assertion f1ssres ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 )

Proof

Step Hyp Ref Expression
1 f1f ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 fssres ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
3 1 2 sylan ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )
4 df-f1 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Fun ◡ 𝐹 ) )
5 funres11 ⊢ ( Fun ◡ 𝐹 → Fun ◡ ( 𝐹 ↾ 𝐶 ) )
6 4 5 simplbiim ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → Fun ◡ ( 𝐹 ↾ 𝐶 ) )
7 6 adantr ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → Fun ◡ ( 𝐹 ↾ 𝐶 ) )
8 df-f1 ⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 ↔ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ∧ Fun ◡ ( 𝐹 ↾ 𝐶 ) ) )
9 3 7 8 sylanbrc ⊢ ( ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 –1-1→ 𝐵 )