Step | Hyp | Ref
| Expression |
1 | | cmsms 24715 |
. . . 4
β’ (πΉ β CMetSp β πΉ β MetSp) |
2 | | msxms 23810 |
. . . 4
β’ (πΉ β MetSp β πΉ β
βMetSp) |
3 | 1, 2 | syl 17 |
. . 3
β’ (πΉ β CMetSp β πΉ β
βMetSp) |
4 | | cmetcusp1.x |
. . . 4
β’ π = (BaseβπΉ) |
5 | | cmetcusp1.d |
. . . 4
β’ π· = ((distβπΉ) βΎ (π Γ π)) |
6 | | cmetcusp1.u |
. . . 4
β’ π = (UnifStβπΉ) |
7 | 4, 5, 6 | xmsusp 23928 |
. . 3
β’ ((π β β
β§ πΉ β βMetSp β§ π = (metUnifβπ·)) β πΉ β UnifSp) |
8 | 3, 7 | syl3an2 1165 |
. 2
β’ ((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β πΉ β UnifSp) |
9 | | simpl3 1194 |
. . . . . . 7
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β π = (metUnifβπ·)) |
10 | 9 | fveq2d 6847 |
. . . . . 6
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β (CauFiluβπ) =
(CauFiluβ(metUnifβπ·))) |
11 | 10 | eleq2d 2824 |
. . . . 5
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β (π β (CauFiluβπ) β π β
(CauFiluβ(metUnifβπ·)))) |
12 | | simpl1 1192 |
. . . . . 6
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β π β β
) |
13 | 4, 5 | cmscmet 24713 |
. . . . . . . . 9
β’ (πΉ β CMetSp β π· β (CMetβπ)) |
14 | | cmetmet 24653 |
. . . . . . . . 9
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
15 | | metxmet 23690 |
. . . . . . . . 9
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
16 | 13, 14, 15 | 3syl 18 |
. . . . . . . 8
β’ (πΉ β CMetSp β π· β (βMetβπ)) |
17 | 16 | 3ad2ant2 1135 |
. . . . . . 7
β’ ((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β π· β (βMetβπ)) |
18 | 17 | adantr 482 |
. . . . . 6
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β π· β (βMetβπ)) |
19 | | simpr 486 |
. . . . . 6
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β π β (Filβπ)) |
20 | | cfilucfil4 24688 |
. . . . . 6
β’ ((π β β
β§ π· β (βMetβπ) β§ π β (Filβπ)) β (π β
(CauFiluβ(metUnifβπ·)) β π β (CauFilβπ·))) |
21 | 12, 18, 19, 20 | syl3anc 1372 |
. . . . 5
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β (π β
(CauFiluβ(metUnifβπ·)) β π β (CauFilβπ·))) |
22 | 11, 21 | bitrd 279 |
. . . 4
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β (π β (CauFiluβπ) β π β (CauFilβπ·))) |
23 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
24 | 23 | iscmet 24651 |
. . . . . . . . . . 11
β’ (π· β (CMetβπ) β (π· β (Metβπ) β§ βπ β (CauFilβπ·)((MetOpenβπ·) fLim π) β β
)) |
25 | 24 | simprbi 498 |
. . . . . . . . . 10
β’ (π· β (CMetβπ) β βπ β (CauFilβπ·)((MetOpenβπ·) fLim π) β β
) |
26 | 13, 25 | syl 17 |
. . . . . . . . 9
β’ (πΉ β CMetSp β
βπ β
(CauFilβπ·)((MetOpenβπ·) fLim π) β β
) |
27 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(TopOpenβπΉ) =
(TopOpenβπΉ) |
28 | 27, 4, 5 | xmstopn 23807 |
. . . . . . . . . . . . 13
β’ (πΉ β βMetSp β
(TopOpenβπΉ) =
(MetOpenβπ·)) |
29 | 3, 28 | syl 17 |
. . . . . . . . . . . 12
β’ (πΉ β CMetSp β
(TopOpenβπΉ) =
(MetOpenβπ·)) |
30 | 29 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (πΉ β CMetSp β
((TopOpenβπΉ) fLim
π) = ((MetOpenβπ·) fLim π)) |
31 | 30 | neeq1d 3004 |
. . . . . . . . . 10
β’ (πΉ β CMetSp β
(((TopOpenβπΉ) fLim
π) β β
β
((MetOpenβπ·) fLim
π) β
β
)) |
32 | 31 | ralbidv 3175 |
. . . . . . . . 9
β’ (πΉ β CMetSp β
(βπ β
(CauFilβπ·)((TopOpenβπΉ) fLim π) β β
β βπ β (CauFilβπ·)((MetOpenβπ·) fLim π) β β
)) |
33 | 26, 32 | mpbird 257 |
. . . . . . . 8
β’ (πΉ β CMetSp β
βπ β
(CauFilβπ·)((TopOpenβπΉ) fLim π) β β
) |
34 | 33 | r19.21bi 3235 |
. . . . . . 7
β’ ((πΉ β CMetSp β§ π β (CauFilβπ·)) β ((TopOpenβπΉ) fLim π) β β
) |
35 | 34 | ex 414 |
. . . . . 6
β’ (πΉ β CMetSp β (π β (CauFilβπ·) β ((TopOpenβπΉ) fLim π) β β
)) |
36 | 35 | 3ad2ant2 1135 |
. . . . 5
β’ ((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β (π β (CauFilβπ·) β ((TopOpenβπΉ) fLim π) β β
)) |
37 | 36 | adantr 482 |
. . . 4
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β (π β (CauFilβπ·) β ((TopOpenβπΉ) fLim π) β β
)) |
38 | 22, 37 | sylbid 239 |
. . 3
β’ (((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β§ π β (Filβπ)) β (π β (CauFiluβπ) β ((TopOpenβπΉ) fLim π) β β
)) |
39 | 38 | ralrimiva 3144 |
. 2
β’ ((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β βπ β (Filβπ)(π β (CauFiluβπ) β ((TopOpenβπΉ) fLim π) β β
)) |
40 | 4, 6, 27 | iscusp2 23657 |
. 2
β’ (πΉ β CUnifSp β (πΉ β UnifSp β§
βπ β
(Filβπ)(π β
(CauFiluβπ) β ((TopOpenβπΉ) fLim π) β β
))) |
41 | 8, 39, 40 | sylanbrc 584 |
1
β’ ((π β β
β§ πΉ β CMetSp β§ π = (metUnifβπ·)) β πΉ β CUnifSp) |