Step | Hyp | Ref
| Expression |
1 | | totbndmet 36944 |
. 2
β’ (π β (TotBndβπ) β π β (Metβπ)) |
2 | | 1rp 12983 |
. . 3
β’ 1 β
β+ |
3 | | istotbnd3 36943 |
. . . 4
β’ (π β (TotBndβπ) β (π β (Metβπ) β§ βπ β β+ βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π)) |
4 | 3 | simprbi 496 |
. . 3
β’ (π β (TotBndβπ) β βπ β β+
βπ£ β (π«
π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π) |
5 | | oveq2 7420 |
. . . . . . 7
β’ (π = 1 β (π₯(ballβπ)π) = (π₯(ballβπ)1)) |
6 | 5 | iuneq2d 5027 |
. . . . . 6
β’ (π = 1 β βͺ π₯ β π£ (π₯(ballβπ)π) = βͺ π₯ β π£ (π₯(ballβπ)1)) |
7 | 6 | eqeq1d 2733 |
. . . . 5
β’ (π = 1 β (βͺ π₯ β π£ (π₯(ballβπ)π) = π β βͺ
π₯ β π£ (π₯(ballβπ)1) = π)) |
8 | 7 | rexbidv 3177 |
. . . 4
β’ (π = 1 β (βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)1) = π)) |
9 | 8 | rspcv 3609 |
. . 3
β’ (1 β
β+ β (βπ β β+ βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)π) = π β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)1) = π)) |
10 | 2, 4, 9 | mpsyl 68 |
. 2
β’ (π β (TotBndβπ) β βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)1) = π) |
11 | | simplll 772 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β π β (Metβπ)) |
12 | | elfpw 9357 |
. . . . . . . . . . . . . 14
β’ (π£ β (π« π β© Fin) β (π£ β π β§ π£ β Fin)) |
13 | 12 | simplbi 497 |
. . . . . . . . . . . . 13
β’ (π£ β (π« π β© Fin) β π£ β π) |
14 | 13 | ad2antrl 725 |
. . . . . . . . . . . 12
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β π£ β π) |
15 | 14 | sselda 3983 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β π§ β π) |
16 | | simpllr 773 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β π¦ β π) |
17 | | metcl 24059 |
. . . . . . . . . . 11
β’ ((π β (Metβπ) β§ π§ β π β§ π¦ β π) β (π§ππ¦) β β) |
18 | 11, 15, 16, 17 | syl3anc 1370 |
. . . . . . . . . 10
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β (π§ππ¦) β β) |
19 | | metge0 24072 |
. . . . . . . . . . 11
β’ ((π β (Metβπ) β§ π§ β π β§ π¦ β π) β 0 β€ (π§ππ¦)) |
20 | 11, 15, 16, 19 | syl3anc 1370 |
. . . . . . . . . 10
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β 0 β€ (π§ππ¦)) |
21 | 18, 20 | ge0p1rpd 13051 |
. . . . . . . . 9
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β ((π§ππ¦) + 1) β
β+) |
22 | 21 | fmpttd 7117 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β (π§ β π£ β¦ ((π§ππ¦) + 1)):π£βΆβ+) |
23 | 22 | frnd 6726 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β
β+) |
24 | 12 | simprbi 496 |
. . . . . . . . . 10
β’ (π£ β (π« π β© Fin) β π£ β Fin) |
25 | | mptfi 9354 |
. . . . . . . . . 10
β’ (π£ β Fin β (π§ β π£ β¦ ((π§ππ¦) + 1)) β Fin) |
26 | | rnfi 9338 |
. . . . . . . . . 10
β’ ((π§ β π£ β¦ ((π§ππ¦) + 1)) β Fin β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β Fin) |
27 | 24, 25, 26 | 3syl 18 |
. . . . . . . . 9
β’ (π£ β (π« π β© Fin) β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β Fin) |
28 | 27 | ad2antrl 725 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β Fin) |
29 | | simplr 766 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β π¦ β π) |
30 | | simprr 770 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β βͺ π₯ β π£ (π₯(ballβπ)1) = π) |
31 | 29, 30 | eleqtrrd 2835 |
. . . . . . . . 9
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β π¦ β βͺ
π₯ β π£ (π₯(ballβπ)1)) |
32 | | ne0i 4335 |
. . . . . . . . 9
β’ (π¦ β βͺ π₯ β π£ (π₯(ballβπ)1) β βͺ π₯ β π£ (π₯(ballβπ)1) β β
) |
33 | | dm0rn0 5925 |
. . . . . . . . . . 11
β’ (dom
(π§ β π£ β¦ ((π§ππ¦) + 1)) = β
β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) = β
) |
34 | | ovex 7445 |
. . . . . . . . . . . . . . 15
β’ ((π§ππ¦) + 1) β V |
35 | | eqid 2731 |
. . . . . . . . . . . . . . 15
β’ (π§ β π£ β¦ ((π§ππ¦) + 1)) = (π§ β π£ β¦ ((π§ππ¦) + 1)) |
36 | 34, 35 | dmmpti 6695 |
. . . . . . . . . . . . . 14
β’ dom
(π§ β π£ β¦ ((π§ππ¦) + 1)) = π£ |
37 | 36 | eqeq1i 2736 |
. . . . . . . . . . . . 13
β’ (dom
(π§ β π£ β¦ ((π§ππ¦) + 1)) = β
β π£ = β
) |
38 | | iuneq1 5014 |
. . . . . . . . . . . . 13
β’ (π£ = β
β βͺ π₯ β π£ (π₯(ballβπ)1) = βͺ
π₯ β β
(π₯(ballβπ)1)) |
39 | 37, 38 | sylbi 216 |
. . . . . . . . . . . 12
β’ (dom
(π§ β π£ β¦ ((π§ππ¦) + 1)) = β
β βͺ π₯ β π£ (π₯(ballβπ)1) = βͺ
π₯ β β
(π₯(ballβπ)1)) |
40 | | 0iun 5067 |
. . . . . . . . . . . 12
β’ βͺ π₯ β β
(π₯(ballβπ)1) = β
|
41 | 39, 40 | eqtrdi 2787 |
. . . . . . . . . . 11
β’ (dom
(π§ β π£ β¦ ((π§ππ¦) + 1)) = β
β βͺ π₯ β π£ (π₯(ballβπ)1) = β
) |
42 | 33, 41 | sylbir 234 |
. . . . . . . . . 10
β’ (ran
(π§ β π£ β¦ ((π§ππ¦) + 1)) = β
β βͺ π₯ β π£ (π₯(ballβπ)1) = β
) |
43 | 42 | necon3i 2972 |
. . . . . . . . 9
β’ (βͺ π₯ β π£ (π₯(ballβπ)1) β β
β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β
) |
44 | 31, 32, 43 | 3syl 18 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β
) |
45 | | rpssre 12986 |
. . . . . . . . 9
β’
β+ β β |
46 | 23, 45 | sstrdi 3995 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β) |
47 | | ltso 11299 |
. . . . . . . . 9
β’ < Or
β |
48 | | fisupcl 9467 |
. . . . . . . . 9
β’ (( <
Or β β§ (ran (π§
β π£ β¦ ((π§ππ¦) + 1)) β Fin β§ ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β
β§ ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β)) β sup(ran
(π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β ran (π§ β π£ β¦ ((π§ππ¦) + 1))) |
49 | 47, 48 | mpan 687 |
. . . . . . . 8
β’ ((ran
(π§ β π£ β¦ ((π§ππ¦) + 1)) β Fin β§ ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β
β§ ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β) β sup(ran
(π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β ran (π§ β π£ β¦ ((π§ππ¦) + 1))) |
50 | 28, 44, 46, 49 | syl3anc 1370 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β ran (π§ β π£ β¦ ((π§ππ¦) + 1))) |
51 | 23, 50 | sseldd 3984 |
. . . . . 6
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β
β+) |
52 | | metxmet 24061 |
. . . . . . . . . . . . . 14
β’ (π β (Metβπ) β π β (βMetβπ)) |
53 | 52 | ad2antrr 723 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β π β (βMetβπ)) |
54 | 53 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β π β (βMetβπ)) |
55 | | 1red 11220 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β 1 β β) |
56 | 46, 50 | sseldd 3984 |
. . . . . . . . . . . . 13
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β
β) |
57 | 56 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β
β) |
58 | 46 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β) |
59 | 44 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β
) |
60 | 28 | adantr 480 |
. . . . . . . . . . . . . . 15
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β Fin) |
61 | | fimaxre2 12164 |
. . . . . . . . . . . . . . 15
β’ ((ran
(π§ β π£ β¦ ((π§ππ¦) + 1)) β β β§ ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β Fin) β βπ β β βπ€ β ran (π§ β π£ β¦ ((π§ππ¦) + 1))π€ β€ π) |
62 | 58, 60, 61 | syl2anc 583 |
. . . . . . . . . . . . . 14
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β βπ β β βπ€ β ran (π§ β π£ β¦ ((π§ππ¦) + 1))π€ β€ π) |
63 | 35 | elrnmpt1 5958 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β π£ β§ ((π§ππ¦) + 1) β V) β ((π§ππ¦) + 1) β ran (π§ β π£ β¦ ((π§ππ¦) + 1))) |
64 | 34, 63 | mpan2 688 |
. . . . . . . . . . . . . . 15
β’ (π§ β π£ β ((π§ππ¦) + 1) β ran (π§ β π£ β¦ ((π§ππ¦) + 1))) |
65 | 64 | adantl 481 |
. . . . . . . . . . . . . 14
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β ((π§ππ¦) + 1) β ran (π§ β π£ β¦ ((π§ππ¦) + 1))) |
66 | | suprub 12180 |
. . . . . . . . . . . . . 14
β’ (((ran
(π§ β π£ β¦ ((π§ππ¦) + 1)) β β β§ ran (π§ β π£ β¦ ((π§ππ¦) + 1)) β β
β§ βπ β β βπ€ β ran (π§ β π£ β¦ ((π§ππ¦) + 1))π€ β€ π) β§ ((π§ππ¦) + 1) β ran (π§ β π£ β¦ ((π§ππ¦) + 1))) β ((π§ππ¦) + 1) β€ sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) |
67 | 58, 59, 62, 65, 66 | syl31anc 1372 |
. . . . . . . . . . . . 13
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β ((π§ππ¦) + 1) β€ sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) |
68 | | leaddsub 11695 |
. . . . . . . . . . . . . 14
β’ (((π§ππ¦) β β β§ 1 β β β§
sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β β)
β (((π§ππ¦) + 1) β€ sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β (π§ππ¦) β€ (sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β
1))) |
69 | 18, 55, 57, 68 | syl3anc 1370 |
. . . . . . . . . . . . 13
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β (((π§ππ¦) + 1) β€ sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β (π§ππ¦) β€ (sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β
1))) |
70 | 67, 69 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β (π§ππ¦) β€ (sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β
1)) |
71 | | blss2 24131 |
. . . . . . . . . . . 12
β’ (((π β (βMetβπ) β§ π§ β π β§ π¦ β π) β§ (1 β β β§ sup(ran
(π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β β β§
(π§ππ¦) β€ (sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β 1))) β
(π§(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
72 | 54, 15, 16, 55, 57, 70, 71 | syl33anc 1384 |
. . . . . . . . . . 11
β’ ((((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β§ π§ β π£) β (π§(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
73 | 72 | ralrimiva 3145 |
. . . . . . . . . 10
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β βπ§ β π£ (π§(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
74 | | nfcv 2902 |
. . . . . . . . . . . 12
β’
β²π§(π₯(ballβπ)1) |
75 | | nfcv 2902 |
. . . . . . . . . . . . 13
β’
β²π§π¦ |
76 | | nfcv 2902 |
. . . . . . . . . . . . 13
β’
β²π§(ballβπ) |
77 | | nfmpt1 5257 |
. . . . . . . . . . . . . . 15
β’
β²π§(π§ β π£ β¦ ((π§ππ¦) + 1)) |
78 | 77 | nfrn 5952 |
. . . . . . . . . . . . . 14
β’
β²π§ran
(π§ β π£ β¦ ((π§ππ¦) + 1)) |
79 | | nfcv 2902 |
. . . . . . . . . . . . . 14
β’
β²π§β |
80 | | nfcv 2902 |
. . . . . . . . . . . . . 14
β’
β²π§
< |
81 | 78, 79, 80 | nfsup 9449 |
. . . . . . . . . . . . 13
β’
β²π§sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) |
82 | 75, 76, 81 | nfov 7442 |
. . . . . . . . . . . 12
β’
β²π§(π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) |
83 | 74, 82 | nfss 3975 |
. . . . . . . . . . 11
β’
β²π§(π₯(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) |
84 | | nfv 1916 |
. . . . . . . . . . 11
β’
β²π₯(π§(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) |
85 | | oveq1 7419 |
. . . . . . . . . . . 12
β’ (π₯ = π§ β (π₯(ballβπ)1) = (π§(ballβπ)1)) |
86 | 85 | sseq1d 4014 |
. . . . . . . . . . 11
β’ (π₯ = π§ β ((π₯(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) β (π§(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )))) |
87 | 83, 84, 86 | cbvralw 3302 |
. . . . . . . . . 10
β’
(βπ₯ β
π£ (π₯(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) β
βπ§ β π£ (π§(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
88 | 73, 87 | sylibr 233 |
. . . . . . . . 9
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β βπ₯ β π£ (π₯(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
89 | | iunss 5049 |
. . . . . . . . 9
β’ (βͺ π₯ β π£ (π₯(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) β
βπ₯ β π£ (π₯(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
90 | 88, 89 | sylibr 233 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β βͺ π₯ β π£ (π₯(ballβπ)1) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
91 | 30, 90 | eqsstrrd 4022 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β π β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
92 | 51 | rpxrd 13022 |
. . . . . . . 8
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β
β*) |
93 | | blssm 24145 |
. . . . . . . 8
β’ ((π β (βMetβπ) β§ π¦ β π β§ sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β
β*) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) β π) |
94 | 53, 29, 92, 93 | syl3anc 1370 |
. . . . . . 7
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < )) β π) |
95 | 91, 94 | eqssd 4000 |
. . . . . 6
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β π = (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
96 | | oveq2 7420 |
. . . . . . 7
β’ (π = sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β (π¦(ballβπ)π) = (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) |
97 | 96 | rspceeqv 3634 |
. . . . . 6
β’ ((sup(ran
(π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ) β
β+ β§ π
= (π¦(ballβπ)sup(ran (π§ β π£ β¦ ((π§ππ¦) + 1)), β, < ))) β
βπ β
β+ π =
(π¦(ballβπ)π)) |
98 | 51, 95, 97 | syl2anc 583 |
. . . . 5
β’ (((π β (Metβπ) β§ π¦ β π) β§ (π£ β (π« π β© Fin) β§ βͺ π₯ β π£ (π₯(ballβπ)1) = π)) β βπ β β+ π = (π¦(ballβπ)π)) |
99 | 98 | rexlimdvaa 3155 |
. . . 4
β’ ((π β (Metβπ) β§ π¦ β π) β (βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)1) = π β βπ β β+ π = (π¦(ballβπ)π))) |
100 | 99 | ralrimdva 3153 |
. . 3
β’ (π β (Metβπ) β (βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)1) = π β βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
101 | | isbnd 36952 |
. . . 4
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
102 | 101 | baib 535 |
. . 3
β’ (π β (Metβπ) β (π β (Bndβπ) β βπ¦ β π βπ β β+ π = (π¦(ballβπ)π))) |
103 | 100, 102 | sylibrd 258 |
. 2
β’ (π β (Metβπ) β (βπ£ β (π« π β© Fin)βͺ π₯ β π£ (π₯(ballβπ)1) = π β π β (Bndβπ))) |
104 | 1, 10, 103 | sylc 65 |
1
β’ (π β (TotBndβπ) β π β (Bndβπ)) |