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

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 )