Step |
Hyp |
Ref |
Expression |
1 |
|
ucnprima.1 |
|- ( ph -> U e. ( UnifOn ` X ) ) |
2 |
|
ucnprima.2 |
|- ( ph -> V e. ( UnifOn ` Y ) ) |
3 |
|
ucnprima.3 |
|- ( ph -> F e. ( U uCn V ) ) |
4 |
|
ucnprima.4 |
|- ( ph -> W e. V ) |
5 |
|
ucnprima.5 |
|- G = ( x e. X , y e. X |-> <. ( F ` x ) , ( F ` y ) >. ) |
6 |
1 2 3 4 5
|
ucnima |
|- ( ph -> E. r e. U ( G " r ) C_ W ) |
7 |
5
|
mpofun |
|- Fun G |
8 |
|
ustssxp |
|- ( ( U e. ( UnifOn ` X ) /\ r e. U ) -> r C_ ( X X. X ) ) |
9 |
1 8
|
sylan |
|- ( ( ph /\ r e. U ) -> r C_ ( X X. X ) ) |
10 |
|
opex |
|- <. ( F ` x ) , ( F ` y ) >. e. _V |
11 |
5 10
|
dmmpo |
|- dom G = ( X X. X ) |
12 |
9 11
|
sseqtrrdi |
|- ( ( ph /\ r e. U ) -> r C_ dom G ) |
13 |
|
funimass3 |
|- ( ( Fun G /\ r C_ dom G ) -> ( ( G " r ) C_ W <-> r C_ ( `' G " W ) ) ) |
14 |
7 12 13
|
sylancr |
|- ( ( ph /\ r e. U ) -> ( ( G " r ) C_ W <-> r C_ ( `' G " W ) ) ) |
15 |
14
|
rexbidva |
|- ( ph -> ( E. r e. U ( G " r ) C_ W <-> E. r e. U r C_ ( `' G " W ) ) ) |
16 |
6 15
|
mpbid |
|- ( ph -> E. r e. U r C_ ( `' G " W ) ) |
17 |
1
|
adantr |
|- ( ( ph /\ r e. U ) -> U e. ( UnifOn ` X ) ) |
18 |
|
simpr |
|- ( ( ph /\ r e. U ) -> r e. U ) |
19 |
|
cnvimass |
|- ( `' G " W ) C_ dom G |
20 |
19 11
|
sseqtri |
|- ( `' G " W ) C_ ( X X. X ) |
21 |
20
|
a1i |
|- ( ( ph /\ r e. U ) -> ( `' G " W ) C_ ( X X. X ) ) |
22 |
|
ustssel |
|- ( ( U e. ( UnifOn ` X ) /\ r e. U /\ ( `' G " W ) C_ ( X X. X ) ) -> ( r C_ ( `' G " W ) -> ( `' G " W ) e. U ) ) |
23 |
17 18 21 22
|
syl3anc |
|- ( ( ph /\ r e. U ) -> ( r C_ ( `' G " W ) -> ( `' G " W ) e. U ) ) |
24 |
23
|
rexlimdva |
|- ( ph -> ( E. r e. U r C_ ( `' G " W ) -> ( `' G " W ) e. U ) ) |
25 |
16 24
|
mpd |
|- ( ph -> ( `' G " W ) e. U ) |