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