Theorem fresin

Description: An identity for the mapping relationship under restriction. (Contributed by Scott Fenton, 4-Sep-2011) (Proof shortened by Mario Carneiro, 26-May-2016)

	Ref	Expression
Assertion	fresin	|- ( F : A --> B -> ( F |` X ) : ( A i^i X ) --> B )

Proof

Step	Hyp	Ref	Expression
1		inss1	|- ( A i^i X ) C_ A
2		fssres	|- ( ( F : A --> B /\ ( A i^i X ) C_ A ) -> ( F |` ( A i^i X ) ) : ( A i^i X ) --> B )
3	1 2	mpan2	|- ( F : A --> B -> ( F |` ( A i^i X ) ) : ( A i^i X ) --> B )
4		resres	|- ( ( F |` A ) |` X ) = ( F |` ( A i^i X ) )
5		ffn	|- ( F : A --> B -> F Fn A )
6		fnresdm	|- ( F Fn A -> ( F |` A ) = F )
7	5 6	syl	|- ( F : A --> B -> ( F |` A ) = F )
8	7	reseq1d	|- ( F : A --> B -> ( ( F |` A ) |` X ) = ( F |` X ) )
9	4 8	eqtr3id	|- ( F : A --> B -> ( F |` ( A i^i X ) ) = ( F |` X ) )
10	9	feq1d	|- ( F : A --> B -> ( ( F |` ( A i^i X ) ) : ( A i^i X ) --> B <-> ( F |` X ) : ( A i^i X ) --> B ) )
11	3 10	mpbid	|- ( F : A --> B -> ( F |` X ) : ( A i^i X ) --> B )