Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’ (πXs(π₯ β πΌ β¦ (π
βπ₯))) = (πXs(π₯ β πΌ β¦ (π
βπ₯))) |
2 | | eqid 2737 |
. . . 4
β’
(Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) = (Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) |
3 | | prdsbnd.v |
. . . 4
β’ π = (Baseβ(π
βπ₯)) |
4 | | prdsbnd.e |
. . . 4
β’ πΈ = ((distβ(π
βπ₯)) βΎ (π Γ π)) |
5 | | eqid 2737 |
. . . 4
β’
(distβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) = (distβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) |
6 | | prdsbnd.s |
. . . 4
β’ (π β π β π) |
7 | | prdsbnd.i |
. . . 4
β’ (π β πΌ β Fin) |
8 | | fvexd 6862 |
. . . 4
β’ ((π β§ π₯ β πΌ) β (π
βπ₯) β V) |
9 | | prdstotbnd.m |
. . . . 5
β’ ((π β§ π₯ β πΌ) β πΈ β (TotBndβπ)) |
10 | | totbndmet 36260 |
. . . . 5
β’ (πΈ β (TotBndβπ) β πΈ β (Metβπ)) |
11 | 9, 10 | syl 17 |
. . . 4
β’ ((π β§ π₯ β πΌ) β πΈ β (Metβπ)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 11 | prdsmet 23739 |
. . 3
β’ (π β (distβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))) β (Metβ(Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))))) |
13 | | prdsbnd.d |
. . . 4
β’ π· = (distβπ) |
14 | | prdsbnd.y |
. . . . . 6
β’ π = (πXsπ
) |
15 | | prdsbnd.r |
. . . . . . . 8
β’ (π β π
Fn πΌ) |
16 | | dffn5 6906 |
. . . . . . . 8
β’ (π
Fn πΌ β π
= (π₯ β πΌ β¦ (π
βπ₯))) |
17 | 15, 16 | sylib 217 |
. . . . . . 7
β’ (π β π
= (π₯ β πΌ β¦ (π
βπ₯))) |
18 | 17 | oveq2d 7378 |
. . . . . 6
β’ (π β (πXsπ
) = (πXs(π₯ β πΌ β¦ (π
βπ₯)))) |
19 | 14, 18 | eqtrid 2789 |
. . . . 5
β’ (π β π = (πXs(π₯ β πΌ β¦ (π
βπ₯)))) |
20 | 19 | fveq2d 6851 |
. . . 4
β’ (π β (distβπ) = (distβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
21 | 13, 20 | eqtrid 2789 |
. . 3
β’ (π β π· = (distβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
22 | | prdsbnd.b |
. . . . 5
β’ π΅ = (Baseβπ) |
23 | 19 | fveq2d 6851 |
. . . . 5
β’ (π β (Baseβπ) = (Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
24 | 22, 23 | eqtrid 2789 |
. . . 4
β’ (π β π΅ = (Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯))))) |
25 | 24 | fveq2d 6851 |
. . 3
β’ (π β (Metβπ΅) =
(Metβ(Baseβ(πXs(π₯ β πΌ β¦ (π
βπ₯)))))) |
26 | 12, 21, 25 | 3eltr4d 2853 |
. 2
β’ (π β π· β (Metβπ΅)) |
27 | 7 | adantr 482 |
. . . . 5
β’ ((π β§ π β β+) β πΌ β Fin) |
28 | | istotbnd3 36259 |
. . . . . . . . . . 11
β’ (πΈ β (TotBndβπ) β (πΈ β (Metβπ) β§ βπ β β+ βπ€ β (π« π β© Fin)βͺ π§ β π€ (π§(ballβπΈ)π) = π)) |
29 | 28 | simprbi 498 |
. . . . . . . . . 10
β’ (πΈ β (TotBndβπ) β βπ β β+
βπ€ β (π«
π β© Fin)βͺ π§ β π€ (π§(ballβπΈ)π) = π) |
30 | 9, 29 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π₯ β πΌ) β βπ β β+ βπ€ β (π« π β© Fin)βͺ π§ β π€ (π§(ballβπΈ)π) = π) |
31 | 30 | r19.21bi 3237 |
. . . . . . . 8
β’ (((π β§ π₯ β πΌ) β§ π β β+) β
βπ€ β (π«
π β© Fin)βͺ π§ β π€ (π§(ballβπΈ)π) = π) |
32 | | df-rex 3075 |
. . . . . . . . 9
β’
(βπ€ β
(π« π β©
Fin)βͺ π§ β π€ (π§(ballβπΈ)π) = π β βπ€(π€ β (π« π β© Fin) β§ βͺ π§ β π€ (π§(ballβπΈ)π) = π)) |
33 | | rexv 3473 |
. . . . . . . . 9
β’
(βπ€ β V
(π€ β (π« π β© Fin) β§ βͺ π§ β π€ (π§(ballβπΈ)π) = π) β βπ€(π€ β (π« π β© Fin) β§ βͺ π§ β π€ (π§(ballβπΈ)π) = π)) |
34 | 32, 33 | bitr4i 278 |
. . . . . . . 8
β’
(βπ€ β
(π« π β©
Fin)βͺ π§ β π€ (π§(ballβπΈ)π) = π β βπ€ β V (π€ β (π« π β© Fin) β§ βͺ π§ β π€ (π§(ballβπΈ)π) = π)) |
35 | 31, 34 | sylib 217 |
. . . . . . 7
β’ (((π β§ π₯ β πΌ) β§ π β β+) β
βπ€ β V (π€ β (π« π β© Fin) β§ βͺ π§ β π€ (π§(ballβπΈ)π) = π)) |
36 | 35 | an32s 651 |
. . . . . 6
β’ (((π β§ π β β+) β§ π₯ β πΌ) β βπ€ β V (π€ β (π« π β© Fin) β§ βͺ π§ β π€ (π§(ballβπΈ)π) = π)) |
37 | 36 | ralrimiva 3144 |
. . . . 5
β’ ((π β§ π β β+) β
βπ₯ β πΌ βπ€ β V (π€ β (π« π β© Fin) β§ βͺ π§ β π€ (π§(ballβπΈ)π) = π)) |
38 | | eleq1 2826 |
. . . . . . 7
β’ (π€ = (πβπ₯) β (π€ β (π« π β© Fin) β (πβπ₯) β (π« π β© Fin))) |
39 | | iuneq1 4975 |
. . . . . . . 8
β’ (π€ = (πβπ₯) β βͺ
π§ β π€ (π§(ballβπΈ)π) = βͺ π§ β (πβπ₯)(π§(ballβπΈ)π)) |
40 | 39 | eqeq1d 2739 |
. . . . . . 7
β’ (π€ = (πβπ₯) β (βͺ
π§ β π€ (π§(ballβπΈ)π) = π β βͺ
π§ β (πβπ₯)(π§(ballβπΈ)π) = π)) |
41 | 38, 40 | anbi12d 632 |
. . . . . 6
β’ (π€ = (πβπ₯) β ((π€ β (π« π β© Fin) β§ βͺ π§ β π€ (π§(ballβπΈ)π) = π) β ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) |
42 | 41 | ac6sfi 9238 |
. . . . 5
β’ ((πΌ β Fin β§ βπ₯ β πΌ βπ€ β V (π€ β (π« π β© Fin) β§ βͺ π§ β π€ (π§(ballβπΈ)π) = π)) β βπ(π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) |
43 | 27, 37, 42 | syl2anc 585 |
. . . 4
β’ ((π β§ π β β+) β
βπ(π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) |
44 | | elfpw 9305 |
. . . . . . . . . . . 12
β’ ((πβπ₯) β (π« π β© Fin) β ((πβπ₯) β π β§ (πβπ₯) β Fin)) |
45 | 44 | simplbi 499 |
. . . . . . . . . . 11
β’ ((πβπ₯) β (π« π β© Fin) β (πβπ₯) β π) |
46 | 45 | adantr 482 |
. . . . . . . . . 10
β’ (((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π) β (πβπ₯) β π) |
47 | 46 | ralimi 3087 |
. . . . . . . . 9
β’
(βπ₯ β
πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π) β βπ₯ β πΌ (πβπ₯) β π) |
48 | 47 | ad2antll 728 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β βπ₯ β πΌ (πβπ₯) β π) |
49 | | ss2ixp 8855 |
. . . . . . . 8
β’
(βπ₯ β
πΌ (πβπ₯) β π β Xπ₯ β πΌ (πβπ₯) β Xπ₯ β πΌ π) |
50 | 48, 49 | syl 17 |
. . . . . . 7
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β Xπ₯ β πΌ (πβπ₯) β Xπ₯ β πΌ π) |
51 | | fnfi 9132 |
. . . . . . . . . . 11
β’ ((π
Fn πΌ β§ πΌ β Fin) β π
β Fin) |
52 | 15, 7, 51 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β π
β Fin) |
53 | 15 | fndmd 6612 |
. . . . . . . . . 10
β’ (π β dom π
= πΌ) |
54 | 14, 6, 52, 22, 53 | prdsbas 17346 |
. . . . . . . . 9
β’ (π β π΅ = Xπ₯ β πΌ (Baseβ(π
βπ₯))) |
55 | 3 | rgenw 3069 |
. . . . . . . . . 10
β’
βπ₯ β
πΌ π = (Baseβ(π
βπ₯)) |
56 | | ixpeq2 8856 |
. . . . . . . . . 10
β’
(βπ₯ β
πΌ π = (Baseβ(π
βπ₯)) β Xπ₯ β πΌ π = Xπ₯ β πΌ (Baseβ(π
βπ₯))) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . 9
β’ Xπ₯ β
πΌ π = Xπ₯ β πΌ (Baseβ(π
βπ₯)) |
58 | 54, 57 | eqtr4di 2795 |
. . . . . . . 8
β’ (π β π΅ = Xπ₯ β πΌ π) |
59 | 58 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β π΅ = Xπ₯ β πΌ π) |
60 | 50, 59 | sseqtrrd 3990 |
. . . . . 6
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β Xπ₯ β πΌ (πβπ₯) β π΅) |
61 | 27 | adantr 482 |
. . . . . . 7
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β πΌ β Fin) |
62 | 44 | simprbi 498 |
. . . . . . . . . 10
β’ ((πβπ₯) β (π« π β© Fin) β (πβπ₯) β Fin) |
63 | 62 | adantr 482 |
. . . . . . . . 9
β’ (((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π) β (πβπ₯) β Fin) |
64 | 63 | ralimi 3087 |
. . . . . . . 8
β’
(βπ₯ β
πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π) β βπ₯ β πΌ (πβπ₯) β Fin) |
65 | 64 | ad2antll 728 |
. . . . . . 7
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β βπ₯ β πΌ (πβπ₯) β Fin) |
66 | | ixpfi 9300 |
. . . . . . 7
β’ ((πΌ β Fin β§ βπ₯ β πΌ (πβπ₯) β Fin) β Xπ₯ β
πΌ (πβπ₯) β Fin) |
67 | 61, 65, 66 | syl2anc 585 |
. . . . . 6
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β Xπ₯ β πΌ (πβπ₯) β Fin) |
68 | | elfpw 9305 |
. . . . . 6
β’ (Xπ₯ β
πΌ (πβπ₯) β (π« π΅ β© Fin) β (Xπ₯ β
πΌ (πβπ₯) β π΅ β§ Xπ₯ β πΌ (πβπ₯) β Fin)) |
69 | 60, 67, 68 | sylanbrc 584 |
. . . . 5
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β Xπ₯ β πΌ (πβπ₯) β (π« π΅ β© Fin)) |
70 | | metxmet 23703 |
. . . . . . . . . . 11
β’ (π· β (Metβπ΅) β π· β (βMetβπ΅)) |
71 | 26, 70 | syl 17 |
. . . . . . . . . 10
β’ (π β π· β (βMetβπ΅)) |
72 | | rpxr 12931 |
. . . . . . . . . 10
β’ (π β β+
β π β
β*) |
73 | | blssm 23787 |
. . . . . . . . . . . . 13
β’ ((π· β (βMetβπ΅) β§ π¦ β π΅ β§ π β β*) β (π¦(ballβπ·)π) β π΅) |
74 | 73 | 3expa 1119 |
. . . . . . . . . . . 12
β’ (((π· β (βMetβπ΅) β§ π¦ β π΅) β§ π β β*) β (π¦(ballβπ·)π) β π΅) |
75 | 74 | an32s 651 |
. . . . . . . . . . 11
β’ (((π· β (βMetβπ΅) β§ π β β*) β§ π¦ β π΅) β (π¦(ballβπ·)π) β π΅) |
76 | 75 | ralrimiva 3144 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ΅) β§ π β β*) β
βπ¦ β π΅ (π¦(ballβπ·)π) β π΅) |
77 | 71, 72, 76 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ π β β+) β
βπ¦ β π΅ (π¦(ballβπ·)π) β π΅) |
78 | 77 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β βπ¦ β π΅ (π¦(ballβπ·)π) β π΅) |
79 | | ssralv 4015 |
. . . . . . . 8
β’ (Xπ₯ β
πΌ (πβπ₯) β π΅ β (βπ¦ β π΅ (π¦(ballβπ·)π) β π΅ β βπ¦ β X π₯ β πΌ (πβπ₯)(π¦(ballβπ·)π) β π΅)) |
80 | 60, 78, 79 | sylc 65 |
. . . . . . 7
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β βπ¦ β X π₯ β πΌ (πβπ₯)(π¦(ballβπ·)π) β π΅) |
81 | | iunss 5010 |
. . . . . . 7
β’ (βͺ π¦ β X π₯ β πΌ (πβπ₯)(π¦(ballβπ·)π) β π΅ β βπ¦ β X π₯ β πΌ (πβπ₯)(π¦(ballβπ·)π) β π΅) |
82 | 80, 81 | sylibr 233 |
. . . . . 6
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β βͺ π¦ β X π₯ β πΌ (πβπ₯)(π¦(ballβπ·)π) β π΅) |
83 | 61 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β πΌ β Fin) |
84 | 59 | eleq2d 2824 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β (π β π΅ β π β Xπ₯ β πΌ π)) |
85 | | vex 3452 |
. . . . . . . . . . . . . . . 16
β’ π β V |
86 | 85 | elixp 8849 |
. . . . . . . . . . . . . . 15
β’ (π β Xπ₯ β
πΌ π β (π Fn πΌ β§ βπ₯ β πΌ (πβπ₯) β π)) |
87 | 86 | simprbi 498 |
. . . . . . . . . . . . . 14
β’ (π β Xπ₯ β
πΌ π β βπ₯ β πΌ (πβπ₯) β π) |
88 | | df-rex 3075 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ§ β
(πβπ₯)(πβπ₯) β (π§(ballβπΈ)π) β βπ§(π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π))) |
89 | | eliun 4963 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πβπ₯) β βͺ
π§ β (πβπ₯)(π§(ballβπΈ)π) β βπ§ β (πβπ₯)(πβπ₯) β (π§(ballβπΈ)π)) |
90 | | rexv 3473 |
. . . . . . . . . . . . . . . . . . . 20
β’
(βπ§ β V
(π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π)) β βπ§(π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π))) |
91 | 88, 89, 90 | 3bitr4i 303 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πβπ₯) β βͺ
π§ β (πβπ₯)(π§(ballβπΈ)π) β βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π))) |
92 | | eleq2 2827 |
. . . . . . . . . . . . . . . . . . 19
β’ (βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π β ((πβπ₯) β βͺ
π§ β (πβπ₯)(π§(ballβπΈ)π) β (πβπ₯) β π)) |
93 | 91, 92 | bitr3id 285 |
. . . . . . . . . . . . . . . . . 18
β’ (βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π β (βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π)) β (πβπ₯) β π)) |
94 | 93 | biimprd 248 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π β ((πβπ₯) β π β βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π)))) |
95 | 94 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π) β ((πβπ₯) β π β βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π)))) |
96 | 95 | ral2imi 3089 |
. . . . . . . . . . . . . . 15
β’
(βπ₯ β
πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π) β (βπ₯ β πΌ (πβπ₯) β π β βπ₯ β πΌ βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π)))) |
97 | 96 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β (βπ₯ β πΌ (πβπ₯) β π β βπ₯ β πΌ βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π)))) |
98 | 87, 97 | syl5 34 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β (π β Xπ₯ β πΌ π β βπ₯ β πΌ βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π)))) |
99 | 84, 98 | sylbid 239 |
. . . . . . . . . . . 12
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β (π β π΅ β βπ₯ β πΌ βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π)))) |
100 | 99 | imp 408 |
. . . . . . . . . . 11
β’ ((((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β βπ₯ β πΌ βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π))) |
101 | | eleq1 2826 |
. . . . . . . . . . . . 13
β’ (π§ = (π¦βπ₯) β (π§ β (πβπ₯) β (π¦βπ₯) β (πβπ₯))) |
102 | | oveq1 7369 |
. . . . . . . . . . . . . 14
β’ (π§ = (π¦βπ₯) β (π§(ballβπΈ)π) = ((π¦βπ₯)(ballβπΈ)π)) |
103 | 102 | eleq2d 2824 |
. . . . . . . . . . . . 13
β’ (π§ = (π¦βπ₯) β ((πβπ₯) β (π§(ballβπΈ)π) β (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π))) |
104 | 101, 103 | anbi12d 632 |
. . . . . . . . . . . 12
β’ (π§ = (π¦βπ₯) β ((π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π)) β ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) |
105 | 104 | ac6sfi 9238 |
. . . . . . . . . . 11
β’ ((πΌ β Fin β§ βπ₯ β πΌ βπ§ β V (π§ β (πβπ₯) β§ (πβπ₯) β (π§(ballβπΈ)π))) β βπ¦(π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) |
106 | 83, 100, 105 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β βπ¦(π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) |
107 | | ffn 6673 |
. . . . . . . . . . . . . . . . 17
β’ (π¦:πΌβΆV β π¦ Fn πΌ) |
108 | | simpl 484 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)) β (π¦βπ₯) β (πβπ₯)) |
109 | 108 | ralimi 3087 |
. . . . . . . . . . . . . . . . 17
β’
(βπ₯ β
πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)) β βπ₯ β πΌ (π¦βπ₯) β (πβπ₯)) |
110 | 107, 109 | anim12i 614 |
. . . . . . . . . . . . . . . 16
β’ ((π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π))) β (π¦ Fn πΌ β§ βπ₯ β πΌ (π¦βπ₯) β (πβπ₯))) |
111 | | vex 3452 |
. . . . . . . . . . . . . . . . 17
β’ π¦ β V |
112 | 111 | elixp 8849 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β Xπ₯ β
πΌ (πβπ₯) β (π¦ Fn πΌ β§ βπ₯ β πΌ (π¦βπ₯) β (πβπ₯))) |
113 | 110, 112 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π))) β π¦ β Xπ₯ β πΌ (πβπ₯)) |
114 | 113 | adantl 483 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β π¦ β Xπ₯ β πΌ (πβπ₯)) |
115 | 84 | biimpa 478 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β π β Xπ₯ β πΌ π) |
116 | | ixpfn 8848 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Xπ₯ β
πΌ π β π Fn πΌ) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β π Fn πΌ) |
118 | 117 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β π Fn πΌ) |
119 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)) β (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)) |
120 | 119 | ralimi 3087 |
. . . . . . . . . . . . . . . . 17
β’
(βπ₯ β
πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)) β βπ₯ β πΌ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)) |
121 | 120 | ad2antll 728 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β βπ₯ β πΌ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)) |
122 | 85 | elixp 8849 |
. . . . . . . . . . . . . . . 16
β’ (π β Xπ₯ β
πΌ ((π¦βπ₯)(ballβπΈ)π) β (π Fn πΌ β§ βπ₯ β πΌ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π))) |
123 | 118, 121,
122 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β π β Xπ₯ β πΌ ((π¦βπ₯)(ballβπΈ)π)) |
124 | | simp-4l 782 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β π) |
125 | 50 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β Xπ₯ β πΌ (πβπ₯) β Xπ₯ β πΌ π) |
126 | 125, 114 | sseldd 3950 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β π¦ β Xπ₯ β πΌ π) |
127 | 124, 58 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β π΅ = Xπ₯ β πΌ π) |
128 | 126, 127 | eleqtrrd 2841 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β π¦ β π΅) |
129 | | simp-4r 783 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β π β β+) |
130 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π¦ = π₯ β (π
βπ¦) = (π
βπ₯)) |
131 | 130 | cbvmptv 5223 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π¦ β πΌ β¦ (π
βπ¦)) = (π₯ β πΌ β¦ (π
βπ₯)) |
132 | 131 | oveq2i 7373 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (πXs(π¦ β πΌ β¦ (π
βπ¦))) = (πXs(π₯ β πΌ β¦ (π
βπ₯))) |
133 | 19, 132 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π = (πXs(π¦ β πΌ β¦ (π
βπ¦)))) |
134 | 133 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (distβπ) = (distβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
135 | 13, 134 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π· = (distβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
136 | 135 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (ballβπ·) =
(ballβ(distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))))) |
137 | 136 | oveqdr 7390 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β (π¦(ballβπ·)π) = (π¦(ballβ(distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))))π)) |
138 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))) = (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))) |
139 | | eqid 2737 |
. . . . . . . . . . . . . . . . . 18
β’
(distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))) = (distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))) |
140 | 6 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β π β π) |
141 | 7 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β πΌ β Fin) |
142 | | fvexd 6862 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π¦ β π΅ β§ π β β+)) β§ π₯ β πΌ) β (π
βπ₯) β V) |
143 | | metxmet 23703 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΈ β (Metβπ) β πΈ β (βMetβπ)) |
144 | 11, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
145 | 144 | adantlr 714 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ (π¦ β π΅ β§ π β β+)) β§ π₯ β πΌ) β πΈ β (βMetβπ)) |
146 | | simprl 770 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β π¦ β π΅) |
147 | 133 | fveq2d 6851 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (Baseβπ) = (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
148 | 22, 147 | eqtrid 2789 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π΅ = (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
149 | 148 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β π΅ = (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
150 | 146, 149 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β π¦ β (Baseβ(πXs(π¦ β πΌ β¦ (π
βπ¦))))) |
151 | 72 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β π β
β*) |
152 | | rpgt0 12934 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β+
β 0 < π) |
153 | 152 | ad2antll 728 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β 0 <
π) |
154 | 132, 138,
3, 4, 139, 140, 141, 142, 145, 150, 151, 153 | prdsbl 23863 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β (π¦(ballβ(distβ(πXs(π¦ β πΌ β¦ (π
βπ¦)))))π) = Xπ₯ β πΌ ((π¦βπ₯)(ballβπΈ)π)) |
155 | 137, 154 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π¦ β π΅ β§ π β β+)) β (π¦(ballβπ·)π) = Xπ₯ β πΌ ((π¦βπ₯)(ballβπΈ)π)) |
156 | 124, 128,
129, 155 | syl12anc 836 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β (π¦(ballβπ·)π) = Xπ₯ β πΌ ((π¦βπ₯)(ballβπΈ)π)) |
157 | 123, 156 | eleqtrrd 2841 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β π β (π¦(ballβπ·)π)) |
158 | 114, 157 | jca 513 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β+)
β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β§ (π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π)))) β (π¦ β Xπ₯ β πΌ (πβπ₯) β§ π β (π¦(ballβπ·)π))) |
159 | 158 | ex 414 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β ((π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π))) β (π¦ β Xπ₯ β πΌ (πβπ₯) β§ π β (π¦(ballβπ·)π)))) |
160 | 159 | eximdv 1921 |
. . . . . . . . . . 11
β’ ((((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β (βπ¦(π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π))) β βπ¦(π¦ β Xπ₯ β πΌ (πβπ₯) β§ π β (π¦(ballβπ·)π)))) |
161 | | df-rex 3075 |
. . . . . . . . . . 11
β’
(βπ¦ β
X π₯
β πΌ (πβπ₯)π β (π¦(ballβπ·)π) β βπ¦(π¦ β Xπ₯ β πΌ (πβπ₯) β§ π β (π¦(ballβπ·)π))) |
162 | 160, 161 | syl6ibr 252 |
. . . . . . . . . 10
β’ ((((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β (βπ¦(π¦:πΌβΆV β§ βπ₯ β πΌ ((π¦βπ₯) β (πβπ₯) β§ (πβπ₯) β ((π¦βπ₯)(ballβπΈ)π))) β βπ¦ β X π₯ β πΌ (πβπ₯)π β (π¦(ballβπ·)π))) |
163 | 106, 162 | mpd 15 |
. . . . . . . . 9
β’ ((((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β§ π β π΅) β βπ¦ β X π₯ β πΌ (πβπ₯)π β (π¦(ballβπ·)π)) |
164 | 163 | ex 414 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β (π β π΅ β βπ¦ β X π₯ β πΌ (πβπ₯)π β (π¦(ballβπ·)π))) |
165 | | eliun 4963 |
. . . . . . . 8
β’ (π β βͺ π¦ β X π₯ β πΌ (πβπ₯)(π¦(ballβπ·)π) β βπ¦ β X π₯ β πΌ (πβπ₯)π β (π¦(ballβπ·)π)) |
166 | 164, 165 | syl6ibr 252 |
. . . . . . 7
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β (π β π΅ β π β βͺ
π¦ β X π₯ β
πΌ (πβπ₯)(π¦(ballβπ·)π))) |
167 | 166 | ssrdv 3955 |
. . . . . 6
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β π΅ β βͺ
π¦ β X π₯ β
πΌ (πβπ₯)(π¦(ballβπ·)π)) |
168 | 82, 167 | eqssd 3966 |
. . . . 5
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β βͺ π¦ β X π₯ β πΌ (πβπ₯)(π¦(ballβπ·)π) = π΅) |
169 | | iuneq1 4975 |
. . . . . . 7
β’ (π£ = Xπ₯ β πΌ (πβπ₯) β βͺ
π¦ β π£ (π¦(ballβπ·)π) = βͺ π¦ β X
π₯ β πΌ (πβπ₯)(π¦(ballβπ·)π)) |
170 | 169 | eqeq1d 2739 |
. . . . . 6
β’ (π£ = Xπ₯ β πΌ (πβπ₯) β (βͺ
π¦ β π£ (π¦(ballβπ·)π) = π΅ β βͺ
π¦ β X π₯ β
πΌ (πβπ₯)(π¦(ballβπ·)π) = π΅)) |
171 | 170 | rspcev 3584 |
. . . . 5
β’ ((Xπ₯ β
πΌ (πβπ₯) β (π« π΅ β© Fin) β§ βͺ π¦ β X π₯ β πΌ (πβπ₯)(π¦(ballβπ·)π) = π΅) β βπ£ β (π« π΅ β© Fin)βͺ π¦ β π£ (π¦(ballβπ·)π) = π΅) |
172 | 69, 168, 171 | syl2anc 585 |
. . . 4
β’ (((π β§ π β β+) β§ (π:πΌβΆV β§ βπ₯ β πΌ ((πβπ₯) β (π« π β© Fin) β§ βͺ π§ β (πβπ₯)(π§(ballβπΈ)π) = π))) β βπ£ β (π« π΅ β© Fin)βͺ π¦ β π£ (π¦(ballβπ·)π) = π΅) |
173 | 43, 172 | exlimddv 1939 |
. . 3
β’ ((π β§ π β β+) β
βπ£ β (π«
π΅ β© Fin)βͺ π¦ β π£ (π¦(ballβπ·)π) = π΅) |
174 | 173 | ralrimiva 3144 |
. 2
β’ (π β βπ β β+ βπ£ β (π« π΅ β© Fin)βͺ π¦ β π£ (π¦(ballβπ·)π) = π΅) |
175 | | istotbnd3 36259 |
. 2
β’ (π· β (TotBndβπ΅) β (π· β (Metβπ΅) β§ βπ β β+ βπ£ β (π« π΅ β© Fin)βͺ π¦ β π£ (π¦(ballβπ·)π) = π΅)) |
176 | 26, 174, 175 | sylanbrc 584 |
1
β’ (π β π· β (TotBndβπ΅)) |