Step |
Hyp |
Ref |
Expression |
1 |
|
dmresexg |
|- ( B e. C -> dom ( A |` B ) e. _V ) |
2 |
1
|
adantl |
|- ( ( Fun A /\ B e. C ) -> dom ( A |` B ) e. _V ) |
3 |
|
df-ima |
|- ( A " B ) = ran ( A |` B ) |
4 |
|
funimaexg |
|- ( ( Fun A /\ B e. C ) -> ( A " B ) e. _V ) |
5 |
3 4
|
eqeltrrid |
|- ( ( Fun A /\ B e. C ) -> ran ( A |` B ) e. _V ) |
6 |
2 5
|
jca |
|- ( ( Fun A /\ B e. C ) -> ( dom ( A |` B ) e. _V /\ ran ( A |` B ) e. _V ) ) |
7 |
|
xpexg |
|- ( ( dom ( A |` B ) e. _V /\ ran ( A |` B ) e. _V ) -> ( dom ( A |` B ) X. ran ( A |` B ) ) e. _V ) |
8 |
|
relres |
|- Rel ( A |` B ) |
9 |
|
relssdmrn |
|- ( Rel ( A |` B ) -> ( A |` B ) C_ ( dom ( A |` B ) X. ran ( A |` B ) ) ) |
10 |
8 9
|
ax-mp |
|- ( A |` B ) C_ ( dom ( A |` B ) X. ran ( A |` B ) ) |
11 |
|
ssexg |
|- ( ( ( A |` B ) C_ ( dom ( A |` B ) X. ran ( A |` B ) ) /\ ( dom ( A |` B ) X. ran ( A |` B ) ) e. _V ) -> ( A |` B ) e. _V ) |
12 |
10 11
|
mpan |
|- ( ( dom ( A |` B ) X. ran ( A |` B ) ) e. _V -> ( A |` B ) e. _V ) |
13 |
6 7 12
|
3syl |
|- ( ( Fun A /\ B e. C ) -> ( A |` B ) e. _V ) |