Metamath Proof Explorer


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 )