Step |
Hyp |
Ref |
Expression |
1 |
|
lebnum.j |
|- J = ( MetOpen ` D ) |
2 |
|
lebnum.d |
|- ( ph -> D e. ( Met ` X ) ) |
3 |
|
lebnum.c |
|- ( ph -> J e. Comp ) |
4 |
|
lebnum.s |
|- ( ph -> U C_ J ) |
5 |
|
lebnum.u |
|- ( ph -> X = U. U ) |
6 |
|
metxmet |
|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) ) |
7 |
2 6
|
syl |
|- ( ph -> D e. ( *Met ` X ) ) |
8 |
1
|
mopnuni |
|- ( D e. ( *Met ` X ) -> X = U. J ) |
9 |
7 8
|
syl |
|- ( ph -> X = U. J ) |
10 |
9 5
|
eqtr3d |
|- ( ph -> U. J = U. U ) |
11 |
|
eqid |
|- U. J = U. J |
12 |
11
|
cmpcov |
|- ( ( J e. Comp /\ U C_ J /\ U. J = U. U ) -> E. w e. ( ~P U i^i Fin ) U. J = U. w ) |
13 |
3 4 10 12
|
syl3anc |
|- ( ph -> E. w e. ( ~P U i^i Fin ) U. J = U. w ) |
14 |
|
1rp |
|- 1 e. RR+ |
15 |
|
simprl |
|- ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> w e. ( ~P U i^i Fin ) ) |
16 |
15
|
elin1d |
|- ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> w e. ~P U ) |
17 |
16
|
elpwid |
|- ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> w C_ U ) |
18 |
17
|
ad2antrr |
|- ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> w C_ U ) |
19 |
|
simplr |
|- ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> X e. w ) |
20 |
18 19
|
sseldd |
|- ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> X e. U ) |
21 |
7
|
ad3antrrr |
|- ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> D e. ( *Met ` X ) ) |
22 |
|
simpr |
|- ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> x e. X ) |
23 |
|
rpxr |
|- ( 1 e. RR+ -> 1 e. RR* ) |
24 |
14 23
|
mp1i |
|- ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> 1 e. RR* ) |
25 |
|
blssm |
|- ( ( D e. ( *Met ` X ) /\ x e. X /\ 1 e. RR* ) -> ( x ( ball ` D ) 1 ) C_ X ) |
26 |
21 22 24 25
|
syl3anc |
|- ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> ( x ( ball ` D ) 1 ) C_ X ) |
27 |
|
sseq2 |
|- ( u = X -> ( ( x ( ball ` D ) 1 ) C_ u <-> ( x ( ball ` D ) 1 ) C_ X ) ) |
28 |
27
|
rspcev |
|- ( ( X e. U /\ ( x ( ball ` D ) 1 ) C_ X ) -> E. u e. U ( x ( ball ` D ) 1 ) C_ u ) |
29 |
20 26 28
|
syl2anc |
|- ( ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) /\ x e. X ) -> E. u e. U ( x ( ball ` D ) 1 ) C_ u ) |
30 |
29
|
ralrimiva |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) -> A. x e. X E. u e. U ( x ( ball ` D ) 1 ) C_ u ) |
31 |
|
oveq2 |
|- ( d = 1 -> ( x ( ball ` D ) d ) = ( x ( ball ` D ) 1 ) ) |
32 |
31
|
sseq1d |
|- ( d = 1 -> ( ( x ( ball ` D ) d ) C_ u <-> ( x ( ball ` D ) 1 ) C_ u ) ) |
33 |
32
|
rexbidv |
|- ( d = 1 -> ( E. u e. U ( x ( ball ` D ) d ) C_ u <-> E. u e. U ( x ( ball ` D ) 1 ) C_ u ) ) |
34 |
33
|
ralbidv |
|- ( d = 1 -> ( A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u <-> A. x e. X E. u e. U ( x ( ball ` D ) 1 ) C_ u ) ) |
35 |
34
|
rspcev |
|- ( ( 1 e. RR+ /\ A. x e. X E. u e. U ( x ( ball ` D ) 1 ) C_ u ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) |
36 |
14 30 35
|
sylancr |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ X e. w ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) |
37 |
2
|
ad2antrr |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> D e. ( Met ` X ) ) |
38 |
3
|
ad2antrr |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> J e. Comp ) |
39 |
17
|
adantr |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> w C_ U ) |
40 |
4
|
ad2antrr |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> U C_ J ) |
41 |
39 40
|
sstrd |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> w C_ J ) |
42 |
9
|
ad2antrr |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> X = U. J ) |
43 |
|
simplrr |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> U. J = U. w ) |
44 |
42 43
|
eqtrd |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> X = U. w ) |
45 |
15
|
elin2d |
|- ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> w e. Fin ) |
46 |
45
|
adantr |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> w e. Fin ) |
47 |
|
simpr |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> -. X e. w ) |
48 |
|
eqid |
|- ( y e. X |-> sum_ k e. w inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) = ( y e. X |-> sum_ k e. w inf ( ran ( z e. ( X \ k ) |-> ( y D z ) ) , RR* , < ) ) |
49 |
|
eqid |
|- ( topGen ` ran (,) ) = ( topGen ` ran (,) ) |
50 |
1 37 38 41 44 46 47 48 49
|
lebnumlem3 |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> E. d e. RR+ A. x e. X E. u e. w ( x ( ball ` D ) d ) C_ u ) |
51 |
|
ssrexv |
|- ( w C_ U -> ( E. u e. w ( x ( ball ` D ) d ) C_ u -> E. u e. U ( x ( ball ` D ) d ) C_ u ) ) |
52 |
39 51
|
syl |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> ( E. u e. w ( x ( ball ` D ) d ) C_ u -> E. u e. U ( x ( ball ` D ) d ) C_ u ) ) |
53 |
52
|
ralimdv |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> ( A. x e. X E. u e. w ( x ( ball ` D ) d ) C_ u -> A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) ) |
54 |
53
|
reximdv |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> ( E. d e. RR+ A. x e. X E. u e. w ( x ( ball ` D ) d ) C_ u -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) ) |
55 |
50 54
|
mpd |
|- ( ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) /\ -. X e. w ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) |
56 |
36 55
|
pm2.61dan |
|- ( ( ph /\ ( w e. ( ~P U i^i Fin ) /\ U. J = U. w ) ) -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) |
57 |
13 56
|
rexlimddv |
|- ( ph -> E. d e. RR+ A. x e. X E. u e. U ( x ( ball ` D ) d ) C_ u ) |