Step |
Hyp |
Ref |
Expression |
1 |
|
bnsscmcl.x |
|- X = ( BaseSet ` U ) |
2 |
|
bnsscmcl.d |
|- D = ( IndMet ` U ) |
3 |
|
bnsscmcl.j |
|- J = ( MetOpen ` D ) |
4 |
|
bnsscmcl.h |
|- H = ( SubSp ` U ) |
5 |
|
bnsscmcl.y |
|- Y = ( BaseSet ` W ) |
6 |
|
bnnv |
|- ( U e. CBan -> U e. NrmCVec ) |
7 |
4
|
sspnv |
|- ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec ) |
8 |
6 7
|
sylan |
|- ( ( U e. CBan /\ W e. H ) -> W e. NrmCVec ) |
9 |
|
eqid |
|- ( IndMet ` W ) = ( IndMet ` W ) |
10 |
5 9
|
iscbn |
|- ( W e. CBan <-> ( W e. NrmCVec /\ ( IndMet ` W ) e. ( CMet ` Y ) ) ) |
11 |
10
|
baib |
|- ( W e. NrmCVec -> ( W e. CBan <-> ( IndMet ` W ) e. ( CMet ` Y ) ) ) |
12 |
8 11
|
syl |
|- ( ( U e. CBan /\ W e. H ) -> ( W e. CBan <-> ( IndMet ` W ) e. ( CMet ` Y ) ) ) |
13 |
5 2 9 4
|
sspims |
|- ( ( U e. NrmCVec /\ W e. H ) -> ( IndMet ` W ) = ( D |` ( Y X. Y ) ) ) |
14 |
6 13
|
sylan |
|- ( ( U e. CBan /\ W e. H ) -> ( IndMet ` W ) = ( D |` ( Y X. Y ) ) ) |
15 |
14
|
eleq1d |
|- ( ( U e. CBan /\ W e. H ) -> ( ( IndMet ` W ) e. ( CMet ` Y ) <-> ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) ) |
16 |
1 2
|
cbncms |
|- ( U e. CBan -> D e. ( CMet ` X ) ) |
17 |
16
|
adantr |
|- ( ( U e. CBan /\ W e. H ) -> D e. ( CMet ` X ) ) |
18 |
3
|
cmetss |
|- ( D e. ( CMet ` X ) -> ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> Y e. ( Clsd ` J ) ) ) |
19 |
17 18
|
syl |
|- ( ( U e. CBan /\ W e. H ) -> ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> Y e. ( Clsd ` J ) ) ) |
20 |
12 15 19
|
3bitrd |
|- ( ( U e. CBan /\ W e. H ) -> ( W e. CBan <-> Y e. ( Clsd ` J ) ) ) |