Step |
Hyp |
Ref |
Expression |
1 |
|
fnssres |
|- ( ( F Fn A /\ B C_ A ) -> ( F |` B ) Fn B ) |
2 |
|
fniinfv |
|- ( ( F |` B ) Fn B -> |^|_ x e. B ( ( F |` B ) ` x ) = |^| ran ( F |` B ) ) |
3 |
1 2
|
syl |
|- ( ( F Fn A /\ B C_ A ) -> |^|_ x e. B ( ( F |` B ) ` x ) = |^| ran ( F |` B ) ) |
4 |
|
fvres |
|- ( x e. B -> ( ( F |` B ) ` x ) = ( F ` x ) ) |
5 |
4
|
iineq2i |
|- |^|_ x e. B ( ( F |` B ) ` x ) = |^|_ x e. B ( F ` x ) |
6 |
5
|
eqcomi |
|- |^|_ x e. B ( F ` x ) = |^|_ x e. B ( ( F |` B ) ` x ) |
7 |
|
df-ima |
|- ( F " B ) = ran ( F |` B ) |
8 |
7
|
inteqi |
|- |^| ( F " B ) = |^| ran ( F |` B ) |
9 |
3 6 8
|
3eqtr4g |
|- ( ( F Fn A /\ B C_ A ) -> |^|_ x e. B ( F ` x ) = |^| ( F " B ) ) |