Step | Hyp | Ref
| Expression |
1 | | df-cau 24772 |
. 2
β’ Cau =
(π β βͺ ran βMet β¦ {π β (dom dom π βpm β) β£
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯)}) |
2 | | dmeq 5903 |
. . . . . 6
β’ (π = π· β dom π = dom π·) |
3 | 2 | dmeqd 5905 |
. . . . 5
β’ (π = π· β dom dom π = dom dom π·) |
4 | | xmetf 23834 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π·:(π Γ π)βΆβ*) |
5 | 4 | fdmd 6728 |
. . . . . . 7
β’ (π· β (βMetβπ) β dom π· = (π Γ π)) |
6 | 5 | dmeqd 5905 |
. . . . . 6
β’ (π· β (βMetβπ) β dom dom π· = dom (π Γ π)) |
7 | | dmxpid 5929 |
. . . . . 6
β’ dom
(π Γ π) = π |
8 | 6, 7 | eqtrdi 2788 |
. . . . 5
β’ (π· β (βMetβπ) β dom dom π· = π) |
9 | 3, 8 | sylan9eqr 2794 |
. . . 4
β’ ((π· β (βMetβπ) β§ π = π·) β dom dom π = π) |
10 | 9 | oveq1d 7423 |
. . 3
β’ ((π· β (βMetβπ) β§ π = π·) β (dom dom π βpm β) = (π βpm
β)) |
11 | | simpr 485 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π = π·) β π = π·) |
12 | 11 | fveq2d 6895 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π = π·) β (ballβπ) = (ballβπ·)) |
13 | 12 | oveqd 7425 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π = π·) β ((πβπ)(ballβπ)π₯) = ((πβπ)(ballβπ·)π₯)) |
14 | 13 | feq3d 6704 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π = π·) β ((π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯) β (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯))) |
15 | 14 | rexbidv 3178 |
. . . 4
β’ ((π· β (βMetβπ) β§ π = π·) β (βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯) β βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯))) |
16 | 15 | ralbidv 3177 |
. . 3
β’ ((π· β (βMetβπ) β§ π = π·) β (βπ₯ β β+ βπ β β€ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯) β βπ₯ β β+ βπ β β€ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯))) |
17 | 10, 16 | rabeqbidv 3449 |
. 2
β’ ((π· β (βMetβπ) β§ π = π·) β {π β (dom dom π βpm β) β£
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯)} = {π β (π βpm β) β£
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)}) |
18 | | fvssunirn 6924 |
. . 3
β’
(βMetβπ)
β βͺ ran βMet |
19 | 18 | sseli 3978 |
. 2
β’ (π· β (βMetβπ) β π· β βͺ ran
βMet) |
20 | | ovex 7441 |
. . . 4
β’ (π βpm β)
β V |
21 | 20 | rabex 5332 |
. . 3
β’ {π β (π βpm β) β£
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)} β V |
22 | 21 | a1i 11 |
. 2
β’ (π· β (βMetβπ) β {π β (π βpm β) β£
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)} β V) |
23 | 1, 17, 19, 22 | fvmptd2 7006 |
1
β’ (π· β (βMetβπ) β (Cauβπ·) = {π β (π βpm β) β£
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)}) |