Step | Hyp | Ref
| Expression |
1 | | eleq1 2822 |
. . . . 5
β’ (π = πΆ β (π β
(CauFiluβ(UnifStβπ)) β πΆ β
(CauFiluβ(UnifStβπ)))) |
2 | | cuspcvg.2 |
. . . . . . . . 9
β’ π½ = (TopOpenβπ) |
3 | 2 | eqcomi 2742 |
. . . . . . . 8
β’
(TopOpenβπ) =
π½ |
4 | 3 | a1i 11 |
. . . . . . 7
β’ (π = πΆ β (TopOpenβπ) = π½) |
5 | | id 22 |
. . . . . . 7
β’ (π = πΆ β π = πΆ) |
6 | 4, 5 | oveq12d 7427 |
. . . . . 6
β’ (π = πΆ β ((TopOpenβπ) fLim π) = (π½ fLim πΆ)) |
7 | 6 | neeq1d 3001 |
. . . . 5
β’ (π = πΆ β (((TopOpenβπ) fLim π) β β
β (π½ fLim πΆ) β β
)) |
8 | 1, 7 | imbi12d 345 |
. . . 4
β’ (π = πΆ β ((π β
(CauFiluβ(UnifStβπ)) β ((TopOpenβπ) fLim π) β β
) β (πΆ β
(CauFiluβ(UnifStβπ)) β (π½ fLim πΆ) β β
))) |
9 | | iscusp 23804 |
. . . . . 6
β’ (π β CUnifSp β (π β UnifSp β§
βπ β
(Filβ(Baseβπ))(π β
(CauFiluβ(UnifStβπ)) β ((TopOpenβπ) fLim π) β β
))) |
10 | 9 | simprbi 498 |
. . . . 5
β’ (π β CUnifSp β
βπ β
(Filβ(Baseβπ))(π β
(CauFiluβ(UnifStβπ)) β ((TopOpenβπ) fLim π) β β
)) |
11 | 10 | adantr 482 |
. . . 4
β’ ((π β CUnifSp β§ πΆ β (Filβπ΅)) β βπ β
(Filβ(Baseβπ))(π β
(CauFiluβ(UnifStβπ)) β ((TopOpenβπ) fLim π) β β
)) |
12 | | simpr 486 |
. . . . 5
β’ ((π β CUnifSp β§ πΆ β (Filβπ΅)) β πΆ β (Filβπ΅)) |
13 | | cuspcvg.1 |
. . . . . 6
β’ π΅ = (Baseβπ) |
14 | 13 | fveq2i 6895 |
. . . . 5
β’
(Filβπ΅) =
(Filβ(Baseβπ)) |
15 | 12, 14 | eleqtrdi 2844 |
. . . 4
β’ ((π β CUnifSp β§ πΆ β (Filβπ΅)) β πΆ β (Filβ(Baseβπ))) |
16 | 8, 11, 15 | rspcdva 3614 |
. . 3
β’ ((π β CUnifSp β§ πΆ β (Filβπ΅)) β (πΆ β
(CauFiluβ(UnifStβπ)) β (π½ fLim πΆ) β β
)) |
17 | 16 | 3impia 1118 |
. 2
β’ ((π β CUnifSp β§ πΆ β (Filβπ΅) β§ πΆ β
(CauFiluβ(UnifStβπ))) β (π½ fLim πΆ) β β
) |
18 | 17 | 3com23 1127 |
1
β’ ((π β CUnifSp β§ πΆ β
(CauFiluβ(UnifStβπ)) β§ πΆ β (Filβπ΅)) β (π½ fLim πΆ) β β
) |