| Step |
Hyp |
Ref |
Expression |
| 1 |
|
totbndmet |
β’ ( π β ( TotBnd β π ) β π β ( Met β π ) ) |
| 2 |
|
1rp |
β’ 1 β β+ |
| 3 |
|
istotbnd3 |
β’ ( π β ( TotBnd β π ) β ( π β ( Met β π ) β§ β π β β+ β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) π ) = π ) ) |
| 4 |
3
|
simprbi |
β’ ( π β ( TotBnd β π ) β β π β β+ β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) π ) = π ) |
| 5 |
|
oveq2 |
β’ ( π = 1 β ( π₯ ( ball β π ) π ) = ( π₯ ( ball β π ) 1 ) ) |
| 6 |
5
|
iuneq2d |
β’ ( π = 1 β βͺ π₯ β π£ ( π₯ ( ball β π ) π ) = βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) ) |
| 7 |
6
|
eqeq1d |
β’ ( π = 1 β ( βͺ π₯ β π£ ( π₯ ( ball β π ) π ) = π β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) |
| 8 |
7
|
rexbidv |
β’ ( π = 1 β ( β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) π ) = π β β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) |
| 9 |
8
|
rspcv |
β’ ( 1 β β+ β ( β π β β+ β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) π ) = π β β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) |
| 10 |
2 4 9
|
mpsyl |
β’ ( π β ( TotBnd β π ) β β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) |
| 11 |
|
simplll |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β π β ( Met β π ) ) |
| 12 |
|
elfpw |
β’ ( π£ β ( π« π β© Fin ) β ( π£ β π β§ π£ β Fin ) ) |
| 13 |
12
|
simplbi |
β’ ( π£ β ( π« π β© Fin ) β π£ β π ) |
| 14 |
13
|
ad2antrl |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β π£ β π ) |
| 15 |
14
|
sselda |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β π§ β π ) |
| 16 |
|
simpllr |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β π¦ β π ) |
| 17 |
|
metcl |
β’ ( ( π β ( Met β π ) β§ π§ β π β§ π¦ β π ) β ( π§ π π¦ ) β β ) |
| 18 |
11 15 16 17
|
syl3anc |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ( π§ π π¦ ) β β ) |
| 19 |
|
metge0 |
β’ ( ( π β ( Met β π ) β§ π§ β π β§ π¦ β π ) β 0 β€ ( π§ π π¦ ) ) |
| 20 |
11 15 16 19
|
syl3anc |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β 0 β€ ( π§ π π¦ ) ) |
| 21 |
18 20
|
ge0p1rpd |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ( ( π§ π π¦ ) + 1 ) β β+ ) |
| 22 |
21
|
fmpttd |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) : π£ βΆ β+ ) |
| 23 |
22
|
frnd |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β+ ) |
| 24 |
12
|
simprbi |
β’ ( π£ β ( π« π β© Fin ) β π£ β Fin ) |
| 25 |
|
mptfi |
β’ ( π£ β Fin β ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β Fin ) |
| 26 |
|
rnfi |
β’ ( ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β Fin β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β Fin ) |
| 27 |
24 25 26
|
3syl |
β’ ( π£ β ( π« π β© Fin ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β Fin ) |
| 28 |
27
|
ad2antrl |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β Fin ) |
| 29 |
|
simplr |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β π¦ β π ) |
| 30 |
|
simprr |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) |
| 31 |
29 30
|
eleqtrrd |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β π¦ β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) ) |
| 32 |
|
ne0i |
β’ ( π¦ β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) β β
) |
| 33 |
|
dm0rn0 |
β’ ( dom ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) = β
β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) = β
) |
| 34 |
|
ovex |
β’ ( ( π§ π π¦ ) + 1 ) β V |
| 35 |
|
eqid |
β’ ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) = ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) |
| 36 |
34 35
|
dmmpti |
β’ dom ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) = π£ |
| 37 |
36
|
eqeq1i |
β’ ( dom ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) = β
β π£ = β
) |
| 38 |
|
iuneq1 |
β’ ( π£ = β
β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = βͺ π₯ β β
( π₯ ( ball β π ) 1 ) ) |
| 39 |
37 38
|
sylbi |
β’ ( dom ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) = β
β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = βͺ π₯ β β
( π₯ ( ball β π ) 1 ) ) |
| 40 |
|
0iun |
β’ βͺ π₯ β β
( π₯ ( ball β π ) 1 ) = β
|
| 41 |
39 40
|
eqtrdi |
β’ ( dom ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) = β
β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = β
) |
| 42 |
33 41
|
sylbir |
β’ ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) = β
β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = β
) |
| 43 |
42
|
necon3i |
β’ ( βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) β β
β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β
) |
| 44 |
31 32 43
|
3syl |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β
) |
| 45 |
|
rpssre |
β’ β+ β β |
| 46 |
23 45
|
sstrdi |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β ) |
| 47 |
|
ltso |
β’ < Or β |
| 48 |
|
fisupcl |
β’ ( ( < Or β β§ ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β Fin β§ ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β
β§ ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β ) ) β sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) ) |
| 49 |
47 48
|
mpan |
β’ ( ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β Fin β§ ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β
β§ ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β ) β sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) ) |
| 50 |
28 44 46 49
|
syl3anc |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) ) |
| 51 |
23 50
|
sseldd |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β β+ ) |
| 52 |
|
metxmet |
β’ ( π β ( Met β π ) β π β ( βMet β π ) ) |
| 53 |
52
|
ad2antrr |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β π β ( βMet β π ) ) |
| 54 |
53
|
adantr |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β π β ( βMet β π ) ) |
| 55 |
|
1red |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β 1 β β ) |
| 56 |
46 50
|
sseldd |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β β ) |
| 57 |
56
|
adantr |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β β ) |
| 58 |
46
|
adantr |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β ) |
| 59 |
44
|
adantr |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β
) |
| 60 |
28
|
adantr |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β Fin ) |
| 61 |
|
fimaxre2 |
β’ ( ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β β§ ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β Fin ) β β π β β β π€ β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) π€ β€ π ) |
| 62 |
58 60 61
|
syl2anc |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β β π β β β π€ β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) π€ β€ π ) |
| 63 |
35
|
elrnmpt1 |
β’ ( ( π§ β π£ β§ ( ( π§ π π¦ ) + 1 ) β V ) β ( ( π§ π π¦ ) + 1 ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) ) |
| 64 |
34 63
|
mpan2 |
β’ ( π§ β π£ β ( ( π§ π π¦ ) + 1 ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) ) |
| 65 |
64
|
adantl |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ( ( π§ π π¦ ) + 1 ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) ) |
| 66 |
|
suprub |
β’ ( ( ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β β§ ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) β β
β§ β π β β β π€ β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) π€ β€ π ) β§ ( ( π§ π π¦ ) + 1 ) β ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) ) β ( ( π§ π π¦ ) + 1 ) β€ sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) |
| 67 |
58 59 62 65 66
|
syl31anc |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ( ( π§ π π¦ ) + 1 ) β€ sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) |
| 68 |
|
leaddsub |
β’ ( ( ( π§ π π¦ ) β β β§ 1 β β β§ sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β β ) β ( ( ( π§ π π¦ ) + 1 ) β€ sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β ( π§ π π¦ ) β€ ( sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β 1 ) ) ) |
| 69 |
18 55 57 68
|
syl3anc |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ( ( ( π§ π π¦ ) + 1 ) β€ sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β ( π§ π π¦ ) β€ ( sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β 1 ) ) ) |
| 70 |
67 69
|
mpbid |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ( π§ π π¦ ) β€ ( sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β 1 ) ) |
| 71 |
|
blss2 |
β’ ( ( ( π β ( βMet β π ) β§ π§ β π β§ π¦ β π ) β§ ( 1 β β β§ sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β β β§ ( π§ π π¦ ) β€ ( sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β 1 ) ) ) β ( π§ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 72 |
54 15 16 55 57 70 71
|
syl33anc |
β’ ( ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β§ π§ β π£ ) β ( π§ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 73 |
72
|
ralrimiva |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β β π§ β π£ ( π§ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 74 |
|
nfcv |
β’ β² π§ ( π₯ ( ball β π ) 1 ) |
| 75 |
|
nfcv |
β’ β² π§ π¦ |
| 76 |
|
nfcv |
β’ β² π§ ( ball β π ) |
| 77 |
|
nfmpt1 |
β’ β² π§ ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) |
| 78 |
77
|
nfrn |
β’ β² π§ ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) |
| 79 |
|
nfcv |
β’ β² π§ β |
| 80 |
|
nfcv |
β’ β² π§ < |
| 81 |
78 79 80
|
nfsup |
β’ β² π§ sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) |
| 82 |
75 76 81
|
nfov |
β’ β² π§ ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) |
| 83 |
74 82
|
nfss |
β’ β² π§ ( π₯ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) |
| 84 |
|
nfv |
β’ β² π₯ ( π§ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) |
| 85 |
|
oveq1 |
β’ ( π₯ = π§ β ( π₯ ( ball β π ) 1 ) = ( π§ ( ball β π ) 1 ) ) |
| 86 |
85
|
sseq1d |
β’ ( π₯ = π§ β ( ( π₯ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) β ( π§ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) ) |
| 87 |
83 84 86
|
cbvralw |
β’ ( β π₯ β π£ ( π₯ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) β β π§ β π£ ( π§ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 88 |
73 87
|
sylibr |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β β π₯ β π£ ( π₯ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 89 |
|
iunss |
β’ ( βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) β β π₯ β π£ ( π₯ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 90 |
88 89
|
sylibr |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 91 |
30 90
|
eqsstrrd |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β π β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 92 |
51
|
rpxrd |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β β* ) |
| 93 |
|
blssm |
β’ ( ( π β ( βMet β π ) β§ π¦ β π β§ sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β β* ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) β π ) |
| 94 |
53 29 92 93
|
syl3anc |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) β π ) |
| 95 |
91 94
|
eqssd |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β π = ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 96 |
|
oveq2 |
β’ ( π = sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β ( π¦ ( ball β π ) π ) = ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) |
| 97 |
96
|
rspceeqv |
β’ ( ( sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) β β+ β§ π = ( π¦ ( ball β π ) sup ( ran ( π§ β π£ β¦ ( ( π§ π π¦ ) + 1 ) ) , β , < ) ) ) β β π β β+ π = ( π¦ ( ball β π ) π ) ) |
| 98 |
51 95 97
|
syl2anc |
β’ ( ( ( π β ( Met β π ) β§ π¦ β π ) β§ ( π£ β ( π« π β© Fin ) β§ βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π ) ) β β π β β+ π = ( π¦ ( ball β π ) π ) ) |
| 99 |
98
|
rexlimdvaa |
β’ ( ( π β ( Met β π ) β§ π¦ β π ) β ( β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π β β π β β+ π = ( π¦ ( ball β π ) π ) ) ) |
| 100 |
99
|
ralrimdva |
β’ ( π β ( Met β π ) β ( β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π β β π¦ β π β π β β+ π = ( π¦ ( ball β π ) π ) ) ) |
| 101 |
|
isbnd |
β’ ( π β ( Bnd β π ) β ( π β ( Met β π ) β§ β π¦ β π β π β β+ π = ( π¦ ( ball β π ) π ) ) ) |
| 102 |
101
|
baib |
β’ ( π β ( Met β π ) β ( π β ( Bnd β π ) β β π¦ β π β π β β+ π = ( π¦ ( ball β π ) π ) ) ) |
| 103 |
100 102
|
sylibrd |
β’ ( π β ( Met β π ) β ( β π£ β ( π« π β© Fin ) βͺ π₯ β π£ ( π₯ ( ball β π ) 1 ) = π β π β ( Bnd β π ) ) ) |
| 104 |
1 10 103
|
sylc |
β’ ( π β ( TotBnd β π ) β π β ( Bnd β π ) ) |