Step |
Hyp |
Ref |
Expression |
1 |
|
df-ima |
|- ( F " A ) = ran ( F |` A ) |
2 |
|
funres |
|- ( Fun F -> Fun ( F |` A ) ) |
3 |
|
funforn |
|- ( Fun ( F |` A ) <-> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) ) |
4 |
2 3
|
sylib |
|- ( Fun F -> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) ) |
5 |
4
|
3ad2ant1 |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) ) |
6 |
|
fof |
|- ( ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) -> ( F |` A ) : dom ( F |` A ) --> ran ( F |` A ) ) |
7 |
5 6
|
syl |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F |` A ) : dom ( F |` A ) --> ran ( F |` A ) ) |
8 |
|
dmres |
|- dom ( F |` A ) = ( A i^i dom F ) |
9 |
|
inss1 |
|- ( A i^i dom F ) C_ A |
10 |
8 9
|
eqsstri |
|- dom ( F |` A ) C_ A |
11 |
|
simp2 |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> A e. V ) |
12 |
|
ssexg |
|- ( ( dom ( F |` A ) C_ A /\ A e. V ) -> dom ( F |` A ) e. _V ) |
13 |
10 11 12
|
sylancr |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> dom ( F |` A ) e. _V ) |
14 |
|
simp3 |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F " A ) e. W ) |
15 |
1 14
|
eqeltrrid |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ran ( F |` A ) e. W ) |
16 |
|
fex2 |
|- ( ( ( F |` A ) : dom ( F |` A ) --> ran ( F |` A ) /\ dom ( F |` A ) e. _V /\ ran ( F |` A ) e. W ) -> ( F |` A ) e. _V ) |
17 |
7 13 15 16
|
syl3anc |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F |` A ) e. _V ) |
18 |
|
fowdom |
|- ( ( ( F |` A ) e. _V /\ ( F |` A ) : dom ( F |` A ) -onto-> ran ( F |` A ) ) -> ran ( F |` A ) ~<_* dom ( F |` A ) ) |
19 |
17 5 18
|
syl2anc |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ran ( F |` A ) ~<_* dom ( F |` A ) ) |
20 |
|
ssdomg |
|- ( A e. V -> ( dom ( F |` A ) C_ A -> dom ( F |` A ) ~<_ A ) ) |
21 |
10 20
|
mpi |
|- ( A e. V -> dom ( F |` A ) ~<_ A ) |
22 |
|
domwdom |
|- ( dom ( F |` A ) ~<_ A -> dom ( F |` A ) ~<_* A ) |
23 |
21 22
|
syl |
|- ( A e. V -> dom ( F |` A ) ~<_* A ) |
24 |
23
|
3ad2ant2 |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> dom ( F |` A ) ~<_* A ) |
25 |
|
wdomtr |
|- ( ( ran ( F |` A ) ~<_* dom ( F |` A ) /\ dom ( F |` A ) ~<_* A ) -> ran ( F |` A ) ~<_* A ) |
26 |
19 24 25
|
syl2anc |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ran ( F |` A ) ~<_* A ) |
27 |
1 26
|
eqbrtrid |
|- ( ( Fun F /\ A e. V /\ ( F " A ) e. W ) -> ( F " A ) ~<_* A ) |