Step | Hyp | Ref
| Expression |
1 | | eqid 2728 |
. 2
β’
(MetOpenβπ·) =
(MetOpenβπ·) |
2 | | hhssims2.1 |
. . 3
β’ π = β¨β¨(
+β βΎ (π» Γ π»)), ( Β·β
βΎ (β Γ π»))β©, (normβ βΎ
π»)β© |
3 | | hhssims2.3 |
. . 3
β’ π· = (IndMetβπ) |
4 | | hhsscms.3 |
. . . 4
β’ π» β
Cβ |
5 | 4 | chshii 31057 |
. . 3
β’ π» β
Sβ |
6 | 2, 3, 5 | hhssmet 31106 |
. 2
β’ π· β (Metβπ») |
7 | | simpl 481 |
. . . . . . . . . 10
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β (Cauβπ·)) |
8 | 2, 3, 5 | hhssims2 31105 |
. . . . . . . . . . 11
β’ π· = ((normβ
β ββ ) βΎ (π» Γ π»)) |
9 | 8 | fveq2i 6905 |
. . . . . . . . . 10
β’
(Cauβπ·) =
(Cauβ((normβ β ββ )
βΎ (π» Γ π»))) |
10 | 7, 9 | eleqtrdi 2839 |
. . . . . . . . 9
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β (Cauβ((normβ
β ββ ) βΎ (π» Γ π»)))) |
11 | | eqid 2728 |
. . . . . . . . . . 11
β’
(normβ β ββ ) =
(normβ β ββ ) |
12 | 11 | hilxmet 31025 |
. . . . . . . . . 10
β’
(normβ β ββ ) β
(βMetβ β) |
13 | | simpr 483 |
. . . . . . . . . 10
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π:ββΆπ») |
14 | | causs 25246 |
. . . . . . . . . 10
β’
(((normβ β ββ ) β
(βMetβ β) β§ π:ββΆπ») β (π β (Cauβ(normβ
β ββ )) β π β (Cauβ((normβ
β ββ ) βΎ (π» Γ π»))))) |
15 | 12, 13, 14 | sylancr 585 |
. . . . . . . . 9
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β (π β (Cauβ(normβ
β ββ )) β π β (Cauβ((normβ
β ββ ) βΎ (π» Γ π»))))) |
16 | 10, 15 | mpbird 256 |
. . . . . . . 8
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β (Cauβ(normβ
β ββ ))) |
17 | 4 | chssii 31061 |
. . . . . . . . . 10
β’ π» β
β |
18 | | fss 6744 |
. . . . . . . . . 10
β’ ((π:ββΆπ» β§ π» β β) β π:ββΆ β) |
19 | 13, 17, 18 | sylancl 584 |
. . . . . . . . 9
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π:ββΆ β) |
20 | | ax-hilex 30829 |
. . . . . . . . . 10
β’ β
β V |
21 | | nnex 12256 |
. . . . . . . . . 10
β’ β
β V |
22 | 20, 21 | elmap 8896 |
. . . . . . . . 9
β’ (π β ( β
βm β) β π:ββΆ β) |
23 | 19, 22 | sylibr 233 |
. . . . . . . 8
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β ( β βm
β)) |
24 | | eqid 2728 |
. . . . . . . . . 10
β’
β¨β¨ +β , Β·β
β©, normββ© = β¨β¨ +β ,
Β·β β©,
normββ© |
25 | 24, 11 | hhims 31002 |
. . . . . . . . . 10
β’
(normβ β ββ ) =
(IndMetββ¨β¨ +β ,
Β·β β©,
normββ©) |
26 | 24, 25 | hhcau 31028 |
. . . . . . . . 9
β’ Cauchy =
((Cauβ(normβ β ββ ))
β© ( β βm β)) |
27 | 26 | elin2 4199 |
. . . . . . . 8
β’ (π β Cauchy β (π β
(Cauβ(normβ β ββ )) β§
π β ( β
βm β))) |
28 | 16, 23, 27 | sylanbrc 581 |
. . . . . . 7
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β Cauchy) |
29 | | ax-hcompl 31032 |
. . . . . . 7
β’ (π β Cauchy β
βπ₯ β β
π
βπ£ π₯) |
30 | | vex 3477 |
. . . . . . . . 9
β’ π β V |
31 | | vex 3477 |
. . . . . . . . 9
β’ π₯ β V |
32 | 30, 31 | breldm 5915 |
. . . . . . . 8
β’ (π βπ£
π₯ β π β dom βπ£
) |
33 | 32 | rexlimivw 3148 |
. . . . . . 7
β’
(βπ₯ β
β π
βπ£ π₯ β π β dom βπ£
) |
34 | 28, 29, 33 | 3syl 18 |
. . . . . 6
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β dom βπ£
) |
35 | | hlimf 31067 |
. . . . . . 7
β’
βπ£ :dom βπ£ βΆ
β |
36 | | ffun 6730 |
. . . . . . 7
β’ (
βπ£ :dom βπ£ βΆ β
β Fun βπ£ ) |
37 | | funfvbrb 7065 |
. . . . . . 7
β’ (Fun
βπ£ β (π β dom βπ£
β π
βπ£ ( βπ£ βπ))) |
38 | 35, 36, 37 | mp2b 10 |
. . . . . 6
β’ (π β dom
βπ£ β π βπ£ (
βπ£ βπ)) |
39 | 34, 38 | sylib 217 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π βπ£ (
βπ£ βπ)) |
40 | | eqid 2728 |
. . . . . . . 8
β’
(MetOpenβ(normβ β
ββ )) = (MetOpenβ(normβ β
ββ )) |
41 | 24, 25, 40 | hhlm 31029 |
. . . . . . 7
β’
βπ£ =
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) |
42 | | resss 6011 |
. . . . . . 7
β’
((βπ‘β(MetOpenβ(normβ
β ββ ))) βΎ ( β βm
β)) β
(βπ‘β(MetOpenβ(normβ β
ββ ))) |
43 | 41, 42 | eqsstri 4016 |
. . . . . 6
β’
βπ£ β
(βπ‘β(MetOpenβ(normβ
β ββ ))) |
44 | 43 | ssbri 5197 |
. . . . 5
β’ (π βπ£ (
βπ£ βπ) β π(βπ‘β(MetOpenβ(normβ
β ββ )))( βπ£ βπ)) |
45 | 39, 44 | syl 17 |
. . . 4
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π(βπ‘β(MetOpenβ(normβ
β ββ )))( βπ£ βπ)) |
46 | 8, 40, 1 | metrest 24453 |
. . . . . . 7
β’
(((normβ β ββ ) β
(βMetβ β) β§ π» β β) β
((MetOpenβ(normβ β ββ ))
βΎt π») =
(MetOpenβπ·)) |
47 | 12, 17, 46 | mp2an 690 |
. . . . . 6
β’
((MetOpenβ(normβ β
ββ )) βΎt π») = (MetOpenβπ·) |
48 | 47 | eqcomi 2737 |
. . . . 5
β’
(MetOpenβπ·) =
((MetOpenβ(normβ β ββ ))
βΎt π») |
49 | | nnuz 12903 |
. . . . 5
β’ β =
(β€β₯β1) |
50 | 4 | a1i 11 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π» β Cβ
) |
51 | 40 | mopntop 24366 |
. . . . . 6
β’
((normβ β ββ ) β
(βMetβ β) β (MetOpenβ(normβ
β ββ )) β Top) |
52 | 12, 51 | mp1i 13 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β
(MetOpenβ(normβ β ββ ))
β Top) |
53 | | fvex 6915 |
. . . . . . 7
β’ (
βπ£ βπ) β V |
54 | 53 | chlimi 31064 |
. . . . . 6
β’ ((π» β
Cβ β§ π:ββΆπ» β§ π βπ£ (
βπ£ βπ)) β ( βπ£
βπ) β π») |
55 | 50, 13, 39, 54 | syl3anc 1368 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β ( βπ£
βπ) β π») |
56 | | 1zzd 12631 |
. . . . 5
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β 1 β β€) |
57 | 48, 49, 50, 52, 55, 56, 13 | lmss 23222 |
. . . 4
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β (π(βπ‘β(MetOpenβ(normβ
β ββ )))( βπ£ βπ) β π(βπ‘β(MetOpenβπ·))( βπ£ βπ))) |
58 | 45, 57 | mpbid 231 |
. . 3
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π(βπ‘β(MetOpenβπ·))( βπ£
βπ)) |
59 | 30, 53 | breldm 5915 |
. . 3
β’ (π(βπ‘β(MetOpenβπ·))( βπ£
βπ) β π β dom
(βπ‘β(MetOpenβπ·))) |
60 | 58, 59 | syl 17 |
. 2
β’ ((π β (Cauβπ·) β§ π:ββΆπ») β π β dom
(βπ‘β(MetOpenβπ·))) |
61 | 1, 6, 60 | iscmet3i 25260 |
1
β’ π· β (CMetβπ») |