Step | Hyp | Ref
| Expression |
1 | | elfvex 6930 |
. 2
β’ (π β (Bndβπ) β π β V) |
2 | | elfvex 6930 |
. . 3
β’ (π β (Metβπ) β π β V) |
3 | 2 | adantr 482 |
. 2
β’ ((π β (Metβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)) β π β V) |
4 | | fveq2 6892 |
. . . . . 6
β’ (π¦ = π β (Metβπ¦) = (Metβπ)) |
5 | | eqeq1 2737 |
. . . . . . . 8
β’ (π¦ = π β (π¦ = (π₯(ballβπ)π) β π = (π₯(ballβπ)π))) |
6 | 5 | rexbidv 3179 |
. . . . . . 7
β’ (π¦ = π β (βπ β β+ π¦ = (π₯(ballβπ)π) β βπ β β+ π = (π₯(ballβπ)π))) |
7 | 6 | raleqbi1dv 3334 |
. . . . . 6
β’ (π¦ = π β (βπ₯ β π¦ βπ β β+ π¦ = (π₯(ballβπ)π) β βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
8 | 4, 7 | rabeqbidv 3450 |
. . . . 5
β’ (π¦ = π β {π β (Metβπ¦) β£ βπ₯ β π¦ βπ β β+ π¦ = (π₯(ballβπ)π)} = {π β (Metβπ) β£ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)}) |
9 | | df-bnd 36647 |
. . . . 5
β’ Bnd =
(π¦ β V β¦ {π β (Metβπ¦) β£ βπ₯ β π¦ βπ β β+ π¦ = (π₯(ballβπ)π)}) |
10 | | fvex 6905 |
. . . . . 6
β’
(Metβπ) β
V |
11 | 10 | rabex 5333 |
. . . . 5
β’ {π β (Metβπ) β£ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)} β V |
12 | 8, 9, 11 | fvmpt 6999 |
. . . 4
β’ (π β V β
(Bndβπ) = {π β (Metβπ) β£ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)}) |
13 | 12 | eleq2d 2820 |
. . 3
β’ (π β V β (π β (Bndβπ) β π β {π β (Metβπ) β£ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)})) |
14 | | fveq2 6892 |
. . . . . . . 8
β’ (π = π β (ballβπ) = (ballβπ)) |
15 | 14 | oveqd 7426 |
. . . . . . 7
β’ (π = π β (π₯(ballβπ)π) = (π₯(ballβπ)π)) |
16 | 15 | eqeq2d 2744 |
. . . . . 6
β’ (π = π β (π = (π₯(ballβπ)π) β π = (π₯(ballβπ)π))) |
17 | 16 | rexbidv 3179 |
. . . . 5
β’ (π = π β (βπ β β+ π = (π₯(ballβπ)π) β βπ β β+ π = (π₯(ballβπ)π))) |
18 | 17 | ralbidv 3178 |
. . . 4
β’ (π = π β (βπ₯ β π βπ β β+ π = (π₯(ballβπ)π) β βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
19 | 18 | elrab 3684 |
. . 3
β’ (π β {π β (Metβπ) β£ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)} β (π β (Metβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |
20 | 13, 19 | bitrdi 287 |
. 2
β’ (π β V β (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π)))) |
21 | 1, 3, 20 | pm5.21nii 380 |
1
β’ (π β (Bndβπ) β (π β (Metβπ) β§ βπ₯ β π βπ β β+ π = (π₯(ballβπ)π))) |