Step | Hyp | Ref
| Expression |
1 | | eqid 2726 |
. 2
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
2 | | hhssims2.1 |
. . 3
β’ π = β¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© |
3 | | hhssims2.3 |
. . 3
β’ π· = (IndMetβπ) |
4 | | hhsscms.3 |
. . . 4
β’ π» β
Cβ |
5 | 4 | chshii 30984 |
. . 3
β’ π» β
Sβ |
6 | 2, 3, 5 | hhssmet 31033 |
. 2
β’ π· β (Metβπ») |
7 | | simpl 482 |
. . . . . . . . . 10
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β (Cauβπ·)) |
8 | 2, 3, 5 | hhssims2 31032 |
. . . . . . . . . . 11
β’ π· = ((normβ
β ββ ) βΎ (π» Γ π»)) |
9 | 8 | fveq2i 6887 |
. . . . . . . . . 10
β’
(Cauβπ·) =
(Cauβ((normβ β ββ )
βΎ (π» Γ π»))) |
10 | 7, 9 | eleqtrdi 2837 |
. . . . . . . . 9
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β (Cauβ((normβ
β ββ ) βΎ (π» Γ π»)))) |
11 | | eqid 2726 |
. . . . . . . . . . 11
β’
(normβ β ββ ) =
(normβ β ββ ) |
12 | 11 | hilxmet 30952 |
. . . . . . . . . 10
β’
(normβ β ββ ) β
(βMetβ β) |
13 | | simpr 484 |
. . . . . . . . . 10
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π:ββΆπ») |
14 | | causs 25176 |
. . . . . . . . . 10
β’
(((normβ β ββ ) β
(βMetβ β) β§ π:ββΆπ») β (π β (Cauβ(normβ
β ββ )) β π β (Cauβ((normβ
β ββ ) βΎ (π» Γ π»))))) |
15 | 12, 13, 14 | sylancr 586 |
. . . . . . . . 9
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β (π β (Cauβ(normβ
β ββ )) β π β (Cauβ((normβ
β ββ ) βΎ (π» Γ π»))))) |
16 | 10, 15 | mpbird 257 |
. . . . . . . 8
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β (Cauβ(normβ
β ββ ))) |
17 | 4 | chssii 30988 |
. . . . . . . . . 10
β’ π» β
β |
18 | | fss 6727 |
. . . . . . . . . 10
β’ ((π:ββΆπ» β§ π» β β) β π:ββΆ β) |
19 | 13, 17, 18 | sylancl 585 |
. . . . . . . . 9
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π:ββΆ β) |
20 | | ax-hilex 30756 |
. . . . . . . . . 10
β’ β
β V |
21 | | nnex 12219 |
. . . . . . . . . 10
β’ β
β V |
22 | 20, 21 | elmap 8864 |
. . . . . . . . 9
β’ (π β ( β
βm β) β π:ββΆ β) |
23 | 19, 22 | sylibr 233 |
. . . . . . . 8
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β ( β βm
β)) |
24 | | eqid 2726 |
. . . . . . . . . 10
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
25 | 24, 11 | hhims 30929 |
. . . . . . . . . 10
β’
(normβ β ββ ) =
(IndMetββ¨β¨ +β ,
Β·β β©,
normββ©) |
26 | 24, 25 | hhcau 30955 |
. . . . . . . . 9
β’ Cauchy =
((Cauβ(normβ β ββ ))
β© ( β βm β)) |
27 | 26 | elin2 4192 |
. . . . . . . 8
β’ (π β Cauchy β (π β
(Cauβ(normβ β ββ )) β§
π β ( β
βm β))) |
28 | 16, 23, 27 | sylanbrc 582 |
. . . . . . 7
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β Cauchy) |
29 | | ax-hcompl 30959 |
. . . . . . 7
β’ (π β Cauchy β
βπ₯ β β
π
βπ£ π₯) |
30 | | vex 3472 |
. . . . . . . . 9
β’ π β V |
31 | | vex 3472 |
. . . . . . . . 9
β’ π₯ β V |
32 | 30, 31 | breldm 5901 |
. . . . . . . 8
β’ (π βπ£
π₯ β π β dom βπ£
) |
33 | 32 | rexlimivw 3145 |
. . . . . . 7
β’
(βπ₯ β
β π
βπ£ π₯ β π β dom βπ£
) |
34 | 28, 29, 33 | 3syl 18 |
. . . . . 6
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β dom βπ£
) |
35 | | hlimf 30994 |
. . . . . . 7
β’
βπ£ :dom βπ£ βΆ
β |
36 | | ffun 6713 |
. . . . . . 7
β’ (
βπ£ :dom βπ£ βΆ β
β Fun βπ£ ) |
37 | | funfvbrb 7045 |
. . . . . . 7
β’ (Fun
βπ£ β (π β dom βπ£
β π
βπ£ ( βπ£ βπ))) |
38 | 35, 36, 37 | mp2b 10 |
. . . . . 6
β’ (π β dom
βπ£ β π βπ£ (
βπ£ βπ)) |
39 | 34, 38 | sylib 217 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π βπ£ (
βπ£ βπ)) |
40 | | eqid 2726 |
. . . . . . . 8
β’
(MetOpenβ(normβ β
ββ )) = (MetOpenβ(normβ β
ββ )) |
41 | 24, 25, 40 | hhlm 30956 |
. . . . . . 7
β’
βπ£ =
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) |
42 | | resss 5999 |
. . . . . . 7
β’
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) β
(βπ‘β(MetOpenβ(normβ β
ββ ))) |
43 | 41, 42 | eqsstri 4011 |
. . . . . 6
β’
βπ£ β
(βπ‘β(MetOpenβ(normβ
β ββ ))) |
44 | 43 | ssbri 5186 |
. . . . 5
β’ (π βπ£ (
βπ£ βπ) β π(βπ‘β(MetOpenβ(normβ
β ββ )))( βπ£ βπ)) |
45 | 39, 44 | syl 17 |
. . . 4
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π(βπ‘β(MetOpenβ(normβ
β ββ )))( βπ£ βπ)) |
46 | 8, 40, 1 | metrest 24383 |
. . . . . . 7
β’
(((normβ β ββ ) β
(βMetβ β) β§ π» β β) β
((MetOpenβ(normβ β ββ ))
βΎt π») =
(MetOpenβπ·)) |
47 | 12, 17, 46 | mp2an 689 |
. . . . . 6
β’
((MetOpenβ(normβ β
ββ )) βΎt π») = (MetOpenβπ·) |
48 | 47 | eqcomi 2735 |
. . . . 5
β’
(MetOpenβπ·) =
((MetOpenβ(normβ β ββ ))
βΎt π») |
49 | | nnuz 12866 |
. . . . 5
β’ β =
(β€β₯β1) |
50 | 4 | a1i 11 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π» β Cβ
) |
51 | 40 | mopntop 24296 |
. . . . . 6
β’
((normβ β ββ ) β
(βMetβ β) β (MetOpenβ(normβ
β ββ )) β Top) |
52 | 12, 51 | mp1i 13 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β
(MetOpenβ(normβ β ββ ))
β Top) |
53 | | fvex 6897 |
. . . . . . 7
β’ (
βπ£ βπ) β V |
54 | 53 | chlimi 30991 |
. . . . . 6
β’ ((π» β
Cβ β§ π:ββΆπ» β§ π βπ£ (
βπ£ βπ)) β ( βπ£
βπ) β π») |
55 | 50, 13, 39, 54 | syl3anc 1368 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β ( βπ£
βπ) β π») |
56 | | 1zzd 12594 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β 1 β β€) |
57 | 48, 49, 50, 52, 55, 56, 13 | lmss 23152 |
. . . 4
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β (π(βπ‘β(MetOpenβ(normβ
β ββ )))( βπ£ βπ) β π(βπ‘β(MetOpenβπ·))( βπ£ βπ))) |
58 | 45, 57 | mpbid 231 |
. . 3
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π(βπ‘β(MetOpenβπ·))( βπ£
βπ)) |
59 | 30, 53 | breldm 5901 |
. . 3
β’ (π(βπ‘β(MetOpenβπ·))( βπ£
βπ) β π β dom
(βπ‘β(MetOpenβπ·))) |
60 | 58, 59 | syl 17 |
. 2
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β dom
(βπ‘β(MetOpenβπ·))) |
61 | 1, 6, 60 | iscmet3i 25190 |
1
β’ π· β (CMetβπ») |