Step |
Hyp |
Ref |
Expression |
1 |
|
fnresin1 |
|- ( F Fn A -> ( F |` ( A i^i B ) ) Fn ( A i^i B ) ) |
2 |
|
resindi |
|- ( F |` ( A i^i B ) ) = ( ( F |` A ) i^i ( F |` B ) ) |
3 |
|
fnresdm |
|- ( F Fn A -> ( F |` A ) = F ) |
4 |
3
|
ineq1d |
|- ( F Fn A -> ( ( F |` A ) i^i ( F |` B ) ) = ( F i^i ( F |` B ) ) ) |
5 |
|
incom |
|- ( ( F |` B ) i^i F ) = ( F i^i ( F |` B ) ) |
6 |
|
resss |
|- ( F |` B ) C_ F |
7 |
|
df-ss |
|- ( ( F |` B ) C_ F <-> ( ( F |` B ) i^i F ) = ( F |` B ) ) |
8 |
6 7
|
mpbi |
|- ( ( F |` B ) i^i F ) = ( F |` B ) |
9 |
5 8
|
eqtr3i |
|- ( F i^i ( F |` B ) ) = ( F |` B ) |
10 |
4 9
|
eqtrdi |
|- ( F Fn A -> ( ( F |` A ) i^i ( F |` B ) ) = ( F |` B ) ) |
11 |
2 10
|
syl5eq |
|- ( F Fn A -> ( F |` ( A i^i B ) ) = ( F |` B ) ) |
12 |
11
|
fneq1d |
|- ( F Fn A -> ( ( F |` ( A i^i B ) ) Fn ( A i^i B ) <-> ( F |` B ) Fn ( A i^i B ) ) ) |
13 |
1 12
|
mpbid |
|- ( F Fn A -> ( F |` B ) Fn ( A i^i B ) ) |