Step |
Hyp |
Ref |
Expression |
1 |
|
hhcms.1 |
|- U = <. <. +h , .h >. , normh >. |
2 |
|
hhcms.2 |
|- D = ( IndMet ` U ) |
3 |
|
eqid |
|- ( MetOpen ` D ) = ( MetOpen ` D ) |
4 |
1 2
|
hhmet |
|- D e. ( Met ` ~H ) |
5 |
1 2
|
hhcau |
|- Cauchy = ( ( Cau ` D ) i^i ( ~H ^m NN ) ) |
6 |
5
|
eleq2i |
|- ( f e. Cauchy <-> f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) ) |
7 |
|
elin |
|- ( f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) <-> ( f e. ( Cau ` D ) /\ f e. ( ~H ^m NN ) ) ) |
8 |
|
ax-hilex |
|- ~H e. _V |
9 |
|
nnex |
|- NN e. _V |
10 |
8 9
|
elmap |
|- ( f e. ( ~H ^m NN ) <-> f : NN --> ~H ) |
11 |
10
|
anbi2i |
|- ( ( f e. ( Cau ` D ) /\ f e. ( ~H ^m NN ) ) <-> ( f e. ( Cau ` D ) /\ f : NN --> ~H ) ) |
12 |
7 11
|
bitri |
|- ( f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) <-> ( f e. ( Cau ` D ) /\ f : NN --> ~H ) ) |
13 |
6 12
|
bitri |
|- ( f e. Cauchy <-> ( f e. ( Cau ` D ) /\ f : NN --> ~H ) ) |
14 |
|
ax-hcompl |
|- ( f e. Cauchy -> E. x e. ~H f ~~>v x ) |
15 |
13 14
|
sylbir |
|- ( ( f e. ( Cau ` D ) /\ f : NN --> ~H ) -> E. x e. ~H f ~~>v x ) |
16 |
1 2 3
|
hhlm |
|- ~~>v = ( ( ~~>t ` ( MetOpen ` D ) ) |` ( ~H ^m NN ) ) |
17 |
16
|
breqi |
|- ( f ~~>v x <-> f ( ( ~~>t ` ( MetOpen ` D ) ) |` ( ~H ^m NN ) ) x ) |
18 |
|
vex |
|- x e. _V |
19 |
18
|
brresi |
|- ( f ( ( ~~>t ` ( MetOpen ` D ) ) |` ( ~H ^m NN ) ) x <-> ( f e. ( ~H ^m NN ) /\ f ( ~~>t ` ( MetOpen ` D ) ) x ) ) |
20 |
17 19
|
bitri |
|- ( f ~~>v x <-> ( f e. ( ~H ^m NN ) /\ f ( ~~>t ` ( MetOpen ` D ) ) x ) ) |
21 |
|
vex |
|- f e. _V |
22 |
21 18
|
breldm |
|- ( f ( ~~>t ` ( MetOpen ` D ) ) x -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) ) |
23 |
20 22
|
simplbiim |
|- ( f ~~>v x -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) ) |
24 |
23
|
rexlimivw |
|- ( E. x e. ~H f ~~>v x -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) ) |
25 |
15 24
|
syl |
|- ( ( f e. ( Cau ` D ) /\ f : NN --> ~H ) -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) ) |
26 |
3 4 25
|
iscmet3i |
|- D e. ( CMet ` ~H ) |