Step | Hyp | Ref
| Expression |
1 | | elfvex 6884 |
. 2
β’ (π· β (CMetβπ) β π β V) |
2 | | elfvex 6884 |
. . 3
β’ (π· β (Metβπ) β π β V) |
3 | 2 | adantr 482 |
. 2
β’ ((π· β (Metβπ) β§ βπ β (CauFilβπ·)(π½ fLim π) β β
) β π β V) |
4 | | fveq2 6846 |
. . . . . 6
β’ (π₯ = π β (Metβπ₯) = (Metβπ)) |
5 | 4 | rabeqdv 3421 |
. . . . 5
β’ (π₯ = π β {π β (Metβπ₯) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
} = {π β (Metβπ) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
}) |
6 | | df-cmet 24644 |
. . . . 5
β’ CMet =
(π₯ β V β¦ {π β (Metβπ₯) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
}) |
7 | | fvex 6859 |
. . . . . 6
β’
(Metβπ) β
V |
8 | 7 | rabex 5293 |
. . . . 5
β’ {π β (Metβπ) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
} β V |
9 | 5, 6, 8 | fvmpt 6952 |
. . . 4
β’ (π β V β
(CMetβπ) = {π β (Metβπ) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
}) |
10 | 9 | eleq2d 2820 |
. . 3
β’ (π β V β (π· β (CMetβπ) β π· β {π β (Metβπ) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
})) |
11 | | fveq2 6846 |
. . . . 5
β’ (π = π· β (CauFilβπ) = (CauFilβπ·)) |
12 | | fveq2 6846 |
. . . . . . . 8
β’ (π = π· β (MetOpenβπ) = (MetOpenβπ·)) |
13 | | iscmet.1 |
. . . . . . . 8
β’ π½ = (MetOpenβπ·) |
14 | 12, 13 | eqtr4di 2791 |
. . . . . . 7
β’ (π = π· β (MetOpenβπ) = π½) |
15 | 14 | oveq1d 7376 |
. . . . . 6
β’ (π = π· β ((MetOpenβπ) fLim π) = (π½ fLim π)) |
16 | 15 | neeq1d 3000 |
. . . . 5
β’ (π = π· β (((MetOpenβπ) fLim π) β β
β (π½ fLim π) β β
)) |
17 | 11, 16 | raleqbidv 3318 |
. . . 4
β’ (π = π· β (βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
β βπ β (CauFilβπ·)(π½ fLim π) β β
)) |
18 | 17 | elrab 3649 |
. . 3
β’ (π· β {π β (Metβπ) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β
} β (π· β (Metβπ) β§ βπ β (CauFilβπ·)(π½ fLim π) β β
)) |
19 | 10, 18 | bitrdi 287 |
. 2
β’ (π β V β (π· β (CMetβπ) β (π· β (Metβπ) β§ βπ β (CauFilβπ·)(π½ fLim π) β β
))) |
20 | 1, 3, 19 | pm5.21nii 380 |
1
β’ (π· β (CMetβπ) β (π· β (Metβπ) β§ βπ β (CauFilβπ·)(π½ fLim π) β β
)) |