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
|
syl5eqr |
|- ( 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 ) |