Step | Hyp | Ref
| Expression |
1 | | fvssunirn 6879 |
. . . 4
β’
(βMetβπ)
β βͺ ran βMet |
2 | 1 | sseli 3944 |
. . 3
β’ (π· β (βMetβπ) β π· β βͺ ran
βMet) |
3 | | dmeq 5863 |
. . . . . . 7
β’ (π = π· β dom π = dom π·) |
4 | 3 | dmeqd 5865 |
. . . . . 6
β’ (π = π· β dom dom π = dom dom π·) |
5 | 4 | fveq2d 6850 |
. . . . 5
β’ (π = π· β (Filβdom dom π) = (Filβdom dom π·)) |
6 | | imaeq1 6012 |
. . . . . . . 8
β’ (π = π· β (π β (π¦ Γ π¦)) = (π· β (π¦ Γ π¦))) |
7 | 6 | sseq1d 3979 |
. . . . . . 7
β’ (π = π· β ((π β (π¦ Γ π¦)) β (0[,)π₯) β (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
8 | 7 | rexbidv 3172 |
. . . . . 6
β’ (π = π· β (βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯) β βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
9 | 8 | ralbidv 3171 |
. . . . 5
β’ (π = π· β (βπ₯ β β+ βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯) β βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯))) |
10 | 5, 9 | rabeqbidv 3423 |
. . . 4
β’ (π = π· β {π β (Filβdom dom π) β£ βπ₯ β β+ βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯)} = {π β (Filβdom dom π·) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)}) |
11 | | df-cfil 24642 |
. . . 4
β’ CauFil =
(π β βͺ ran βMet β¦ {π β (Filβdom dom π) β£ βπ₯ β β+ βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯)}) |
12 | | fvex 6859 |
. . . . 5
β’
(Filβdom dom π·) β V |
13 | 12 | rabex 5293 |
. . . 4
β’ {π β (Filβdom dom π·) β£ βπ₯ β β+
βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)} β V |
14 | 10, 11, 13 | fvmpt 6952 |
. . 3
β’ (π· β βͺ ran βMet β (CauFilβπ·) = {π β (Filβdom dom π·) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)}) |
15 | 2, 14 | syl 17 |
. 2
β’ (π· β (βMetβπ) β (CauFilβπ·) = {π β (Filβdom dom π·) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)}) |
16 | | xmetdmdm 23711 |
. . . 4
β’ (π· β (βMetβπ) β π = dom dom π·) |
17 | 16 | fveq2d 6850 |
. . 3
β’ (π· β (βMetβπ) β (Filβπ) = (Filβdom dom π·)) |
18 | 17 | rabeqdv 3421 |
. 2
β’ (π· β (βMetβπ) β {π β (Filβπ) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)} = {π β (Filβdom dom π·) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)}) |
19 | 15, 18 | eqtr4d 2776 |
1
β’ (π· β (βMetβπ) β (CauFilβπ·) = {π β (Filβπ) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)}) |