Metamath Proof Explorer

Theorem fssres

Description: Restriction of a function with a subclass of its domain. (Contributed by NM, 23-Sep-2004)

Ref Expression
Assertion fssres ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )

Proof

Step Hyp Ref Expression
1 df-f ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
2 fnssres ⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) Fn 𝐶 )
3 resss ⊢ ( 𝐹 ↾ 𝐶 ) ⊆ 𝐹
4 3 rnssi ⊢ ran ( 𝐹 ↾ 𝐶 ) ⊆ ran 𝐹
5 sstr ⊢ ( ( ran ( 𝐹 ↾ 𝐶 ) ⊆ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) → ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 )
6 4 5 mpan ⊢ ( ran 𝐹 ⊆ 𝐵 → ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 )
7 2 6 anim12i ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ 𝐶 ⊆ 𝐴 ) ∧ ran 𝐹 ⊆ 𝐵 ) → ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) )
8 7 an32s ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) )
9 1 8 sylanb ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) )
10 df-f ⊢ ( ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 ↔ ( ( 𝐹 ↾ 𝐶 ) Fn 𝐶 ∧ ran ( 𝐹 ↾ 𝐶 ) ⊆ 𝐵 ) )
11 9 10 sylibr ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) → ( 𝐹 ↾ 𝐶 ) : 𝐶 ⟶ 𝐵 )