Step | Hyp | Ref
| Expression |
1 | | elfvex 6880 |
. 2
β’ (π β (TotBndβπ) β π β V) |
2 | | elfvex 6880 |
. . 3
β’ (π β (Metβπ) β π β V) |
3 | 2 | adantr 481 |
. 2
β’ ((π β (Metβπ) β§ βπ β β+
βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))) β π β V) |
4 | | fveq2 6842 |
. . . . . 6
β’ (π¦ = π β (Metβπ¦) = (Metβπ)) |
5 | | eqeq2 2748 |
. . . . . . . . 9
β’ (π¦ = π β (βͺ π£ = π¦ β βͺ π£ = π)) |
6 | | rexeq 3310 |
. . . . . . . . . 10
β’ (π¦ = π β (βπ₯ β π¦ π = (π₯(ballβπ)π) β βπ₯ β π π = (π₯(ballβπ)π))) |
7 | 6 | ralbidv 3174 |
. . . . . . . . 9
β’ (π¦ = π β (βπ β π£ βπ₯ β π¦ π = (π₯(ballβπ)π) β βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))) |
8 | 5, 7 | anbi12d 631 |
. . . . . . . 8
β’ (π¦ = π β ((βͺ π£ = π¦ β§ βπ β π£ βπ₯ β π¦ π = (π₯(ballβπ)π)) β (βͺ π£ = π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
9 | 8 | rexbidv 3175 |
. . . . . . 7
β’ (π¦ = π β (βπ£ β Fin (βͺ
π£ = π¦ β§ βπ β π£ βπ₯ β π¦ π = (π₯(ballβπ)π)) β βπ£ β Fin (βͺ
π£ = π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
10 | 9 | ralbidv 3174 |
. . . . . 6
β’ (π¦ = π β (βπ β β+ βπ£ β Fin (βͺ π£ =
π¦ β§ βπ β π£ βπ₯ β π¦ π = (π₯(ballβπ)π)) β βπ β β+ βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
11 | 4, 10 | rabeqbidv 3424 |
. . . . 5
β’ (π¦ = π β {π β (Metβπ¦) β£ βπ β β+ βπ£ β Fin (βͺ π£ =
π¦ β§ βπ β π£ βπ₯ β π¦ π = (π₯(ballβπ)π))} = {π β (Metβπ) β£ βπ β β+ βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))}) |
12 | | df-totbnd 36227 |
. . . . 5
β’ TotBnd =
(π¦ β V β¦ {π β (Metβπ¦) β£ βπ β β+
βπ£ β Fin (βͺ π£ =
π¦ β§ βπ β π£ βπ₯ β π¦ π = (π₯(ballβπ)π))}) |
13 | | fvex 6855 |
. . . . . 6
β’
(Metβπ) β
V |
14 | 13 | rabex 5289 |
. . . . 5
β’ {π β (Metβπ) β£ βπ β β+
βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))} β V |
15 | 11, 12, 14 | fvmpt 6948 |
. . . 4
β’ (π β V β
(TotBndβπ) = {π β (Metβπ) β£ βπ β β+
βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))}) |
16 | 15 | eleq2d 2823 |
. . 3
β’ (π β V β (π β (TotBndβπ) β π β {π β (Metβπ) β£ βπ β β+ βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))})) |
17 | | fveq2 6842 |
. . . . . . . . . . 11
β’ (π = π β (ballβπ) = (ballβπ)) |
18 | 17 | oveqd 7374 |
. . . . . . . . . 10
β’ (π = π β (π₯(ballβπ)π) = (π₯(ballβπ)π)) |
19 | 18 | eqeq2d 2747 |
. . . . . . . . 9
β’ (π = π β (π = (π₯(ballβπ)π) β π = (π₯(ballβπ)π))) |
20 | 19 | rexbidv 3175 |
. . . . . . . 8
β’ (π = π β (βπ₯ β π π = (π₯(ballβπ)π) β βπ₯ β π π = (π₯(ballβπ)π))) |
21 | 20 | ralbidv 3174 |
. . . . . . 7
β’ (π = π β (βπ β π£ βπ₯ β π π = (π₯(ballβπ)π) β βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))) |
22 | 21 | anbi2d 629 |
. . . . . 6
β’ (π = π β ((βͺ π£ = π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)) β (βͺ π£ = π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
23 | 22 | rexbidv 3175 |
. . . . 5
β’ (π = π β (βπ£ β Fin (βͺ
π£ = π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)) β βπ£ β Fin (βͺ
π£ = π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
24 | 23 | ralbidv 3174 |
. . . 4
β’ (π = π β (βπ β β+ βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)) β βπ β β+ βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
25 | 24 | elrab 3645 |
. . 3
β’ (π β {π β (Metβπ) β£ βπ β β+ βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))} β (π β (Metβπ) β§ βπ β β+ βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |
26 | 16, 25 | bitrdi 286 |
. 2
β’ (π β V β (π β (TotBndβπ) β (π β (Metβπ) β§ βπ β β+ βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π))))) |
27 | 1, 3, 26 | pm5.21nii 379 |
1
β’ (π β (TotBndβπ) β (π β (Metβπ) β§ βπ β β+ βπ£ β Fin (βͺ π£ =
π β§ βπ β π£ βπ₯ β π π = (π₯(ballβπ)π)))) |