Step | Hyp | Ref
| Expression |
1 | | iscusp 23804 |
. 2
β’ (π β CUnifSp β (π β UnifSp β§
βπ β
(Filβ(Baseβπ))(π β
(CauFiluβ(UnifStβπ)) β ((TopOpenβπ) fLim π) β β
))) |
2 | | iscusp2.1 |
. . . . 5
β’ π΅ = (Baseβπ) |
3 | 2 | fveq2i 6895 |
. . . 4
β’
(Filβπ΅) =
(Filβ(Baseβπ)) |
4 | | iscusp2.2 |
. . . . . . 7
β’ π = (UnifStβπ) |
5 | 4 | fveq2i 6895 |
. . . . . 6
β’
(CauFiluβπ) =
(CauFiluβ(UnifStβπ)) |
6 | 5 | eleq2i 2826 |
. . . . 5
β’ (π β
(CauFiluβπ) β π β
(CauFiluβ(UnifStβπ))) |
7 | | iscusp2.3 |
. . . . . . 7
β’ π½ = (TopOpenβπ) |
8 | 7 | oveq1i 7419 |
. . . . . 6
β’ (π½ fLim π) = ((TopOpenβπ) fLim π) |
9 | 8 | neeq1i 3006 |
. . . . 5
β’ ((π½ fLim π) β β
β ((TopOpenβπ) fLim π) β β
) |
10 | 6, 9 | imbi12i 351 |
. . . 4
β’ ((π β
(CauFiluβπ) β (π½ fLim π) β β
) β (π β
(CauFiluβ(UnifStβπ)) β ((TopOpenβπ) fLim π) β β
)) |
11 | 3, 10 | raleqbii 3339 |
. . 3
β’
(βπ β
(Filβπ΅)(π β
(CauFiluβπ) β (π½ fLim π) β β
) β βπ β
(Filβ(Baseβπ))(π β
(CauFiluβ(UnifStβπ)) β ((TopOpenβπ) fLim π) β β
)) |
12 | 11 | anbi2i 624 |
. 2
β’ ((π β UnifSp β§
βπ β
(Filβπ΅)(π β
(CauFiluβπ) β (π½ fLim π) β β
)) β (π β UnifSp β§ βπ β
(Filβ(Baseβπ))(π β
(CauFiluβ(UnifStβπ)) β ((TopOpenβπ) fLim π) β β
))) |
13 | 1, 12 | bitr4i 278 |
1
β’ (π β CUnifSp β (π β UnifSp β§
βπ β
(Filβπ΅)(π β
(CauFiluβπ) β (π½ fLim π) β β
))) |