Step |
Hyp |
Ref |
Expression |
1 |
|
mreclatBAD. |
|- ( ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) e. ( Moore ` U. ( TopOpen ` W ) ) -> ( toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat ) |
2 |
|
fvex |
|- ( TopOpen ` W ) e. _V |
3 |
2
|
uniex |
|- U. ( TopOpen ` W ) e. _V |
4 |
|
mremre |
|- ( U. ( TopOpen ` W ) e. _V -> ( Moore ` U. ( TopOpen ` W ) ) e. ( Moore ` ~P U. ( TopOpen ` W ) ) ) |
5 |
3 4
|
mp1i |
|- ( W e. ( TopSp i^i LMod ) -> ( Moore ` U. ( TopOpen ` W ) ) e. ( Moore ` ~P U. ( TopOpen ` W ) ) ) |
6 |
|
elinel2 |
|- ( W e. ( TopSp i^i LMod ) -> W e. LMod ) |
7 |
|
eqid |
|- ( Base ` W ) = ( Base ` W ) |
8 |
|
eqid |
|- ( LSubSp ` W ) = ( LSubSp ` W ) |
9 |
7 8
|
lssmre |
|- ( W e. LMod -> ( LSubSp ` W ) e. ( Moore ` ( Base ` W ) ) ) |
10 |
6 9
|
syl |
|- ( W e. ( TopSp i^i LMod ) -> ( LSubSp ` W ) e. ( Moore ` ( Base ` W ) ) ) |
11 |
|
elinel1 |
|- ( W e. ( TopSp i^i LMod ) -> W e. TopSp ) |
12 |
|
eqid |
|- ( TopOpen ` W ) = ( TopOpen ` W ) |
13 |
7 12
|
tpsuni |
|- ( W e. TopSp -> ( Base ` W ) = U. ( TopOpen ` W ) ) |
14 |
13
|
fveq2d |
|- ( W e. TopSp -> ( Moore ` ( Base ` W ) ) = ( Moore ` U. ( TopOpen ` W ) ) ) |
15 |
11 14
|
syl |
|- ( W e. ( TopSp i^i LMod ) -> ( Moore ` ( Base ` W ) ) = ( Moore ` U. ( TopOpen ` W ) ) ) |
16 |
10 15
|
eleqtrd |
|- ( W e. ( TopSp i^i LMod ) -> ( LSubSp ` W ) e. ( Moore ` U. ( TopOpen ` W ) ) ) |
17 |
12
|
tpstop |
|- ( W e. TopSp -> ( TopOpen ` W ) e. Top ) |
18 |
|
eqid |
|- U. ( TopOpen ` W ) = U. ( TopOpen ` W ) |
19 |
18
|
cldmre |
|- ( ( TopOpen ` W ) e. Top -> ( Clsd ` ( TopOpen ` W ) ) e. ( Moore ` U. ( TopOpen ` W ) ) ) |
20 |
11 17 19
|
3syl |
|- ( W e. ( TopSp i^i LMod ) -> ( Clsd ` ( TopOpen ` W ) ) e. ( Moore ` U. ( TopOpen ` W ) ) ) |
21 |
|
mreincl |
|- ( ( ( Moore ` U. ( TopOpen ` W ) ) e. ( Moore ` ~P U. ( TopOpen ` W ) ) /\ ( LSubSp ` W ) e. ( Moore ` U. ( TopOpen ` W ) ) /\ ( Clsd ` ( TopOpen ` W ) ) e. ( Moore ` U. ( TopOpen ` W ) ) ) -> ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) e. ( Moore ` U. ( TopOpen ` W ) ) ) |
22 |
5 16 20 21
|
syl3anc |
|- ( W e. ( TopSp i^i LMod ) -> ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) e. ( Moore ` U. ( TopOpen ` W ) ) ) |
23 |
22 1
|
syl |
|- ( W e. ( TopSp i^i LMod ) -> ( toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat ) |