| Step |
Hyp |
Ref |
Expression |
| 1 |
|
imassrn |
|- ( V " { P } ) C_ ran V |
| 2 |
|
ustssxp |
|- ( ( U e. ( UnifOn ` X ) /\ V e. U ) -> V C_ ( X X. X ) ) |
| 3 |
2
|
3adant3 |
|- ( ( U e. ( UnifOn ` X ) /\ V e. U /\ P e. X ) -> V C_ ( X X. X ) ) |
| 4 |
|
rnss |
|- ( V C_ ( X X. X ) -> ran V C_ ran ( X X. X ) ) |
| 5 |
|
rnxpid |
|- ran ( X X. X ) = X |
| 6 |
4 5
|
sseqtrdi |
|- ( V C_ ( X X. X ) -> ran V C_ X ) |
| 7 |
3 6
|
syl |
|- ( ( U e. ( UnifOn ` X ) /\ V e. U /\ P e. X ) -> ran V C_ X ) |
| 8 |
1 7
|
sstrid |
|- ( ( U e. ( UnifOn ` X ) /\ V e. U /\ P e. X ) -> ( V " { P } ) C_ X ) |