Step |
Hyp |
Ref |
Expression |
1 |
|
f2ndres |
|- ( 2nd |` ( A X. B ) ) : ( A X. B ) --> B |
2 |
|
fssxp |
|- ( F : A --> B -> F C_ ( A X. B ) ) |
3 |
|
fssres |
|- ( ( ( 2nd |` ( A X. B ) ) : ( A X. B ) --> B /\ F C_ ( A X. B ) ) -> ( ( 2nd |` ( A X. B ) ) |` F ) : F --> B ) |
4 |
1 2 3
|
sylancr |
|- ( F : A --> B -> ( ( 2nd |` ( A X. B ) ) |` F ) : F --> B ) |
5 |
2
|
resabs1d |
|- ( F : A --> B -> ( ( 2nd |` ( A X. B ) ) |` F ) = ( 2nd |` F ) ) |
6 |
5
|
eqcomd |
|- ( F : A --> B -> ( 2nd |` F ) = ( ( 2nd |` ( A X. B ) ) |` F ) ) |
7 |
6
|
feq1d |
|- ( F : A --> B -> ( ( 2nd |` F ) : F --> B <-> ( ( 2nd |` ( A X. B ) ) |` F ) : F --> B ) ) |
8 |
4 7
|
mpbird |
|- ( F : A --> B -> ( 2nd |` F ) : F --> B ) |