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

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 ⊢ F : A ⟶ B ∧ C ⊆ A → F ↾ C : C ⟶ B

Proof

Step Hyp Ref Expression
1 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
2 fnssres ⊢ F Fn A ∧ C ⊆ A → F ↾ C Fn C
3 resss ⊢ F ↾ C ⊆ F
4 3 rnssi ⊢ ran ⁡ F ↾ C ⊆ ran ⁡ F
5 sstr ⊢ ran ⁡ F ↾ C ⊆ ran ⁡ F ∧ ran ⁡ F ⊆ B → ran ⁡ F ↾ C ⊆ B
6 4 5 mpan ⊢ ran ⁡ F ⊆ B → ran ⁡ F ↾ C ⊆ B
7 2 6 anim12i ⊢ F Fn A ∧ C ⊆ A ∧ ran ⁡ F ⊆ B → F ↾ C Fn C ∧ ran ⁡ F ↾ C ⊆ B
8 7 an32s ⊢ F Fn A ∧ ran ⁡ F ⊆ B ∧ C ⊆ A → F ↾ C Fn C ∧ ran ⁡ F ↾ C ⊆ B
9 1 8 sylanb ⊢ F : A ⟶ B ∧ C ⊆ A → F ↾ C Fn C ∧ ran ⁡ F ↾ C ⊆ B
10 df-f ⊢ F ↾ C : C ⟶ B ↔ F ↾ C Fn C ∧ ran ⁡ F ↾ C ⊆ B
11 9 10 sylibr ⊢ F : A ⟶ B ∧ C ⊆ A → F ↾ C : C ⟶ B