Step |
Hyp |
Ref |
Expression |
1 |
|
mreclatBAD. |
⊢ ( ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ∈ ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) → ( toInc ‘ ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ) ∈ CLat ) |
2 |
|
fvex |
⊢ ( TopOpen ‘ 𝑊 ) ∈ V |
3 |
2
|
uniex |
⊢ ∪ ( TopOpen ‘ 𝑊 ) ∈ V |
4 |
|
mremre |
⊢ ( ∪ ( TopOpen ‘ 𝑊 ) ∈ V → ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ∈ ( Moore ‘ 𝒫 ∪ ( TopOpen ‘ 𝑊 ) ) ) |
5 |
3 4
|
mp1i |
⊢ ( 𝑊 ∈ ( TopSp ∩ LMod ) → ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ∈ ( Moore ‘ 𝒫 ∪ ( TopOpen ‘ 𝑊 ) ) ) |
6 |
|
elinel2 |
⊢ ( 𝑊 ∈ ( TopSp ∩ LMod ) → 𝑊 ∈ LMod ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) |
8 |
|
eqid |
⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 ) |
9 |
7 8
|
lssmre |
⊢ ( 𝑊 ∈ LMod → ( LSubSp ‘ 𝑊 ) ∈ ( Moore ‘ ( Base ‘ 𝑊 ) ) ) |
10 |
6 9
|
syl |
⊢ ( 𝑊 ∈ ( TopSp ∩ LMod ) → ( LSubSp ‘ 𝑊 ) ∈ ( Moore ‘ ( Base ‘ 𝑊 ) ) ) |
11 |
|
elinel1 |
⊢ ( 𝑊 ∈ ( TopSp ∩ LMod ) → 𝑊 ∈ TopSp ) |
12 |
|
eqid |
⊢ ( TopOpen ‘ 𝑊 ) = ( TopOpen ‘ 𝑊 ) |
13 |
7 12
|
tpsuni |
⊢ ( 𝑊 ∈ TopSp → ( Base ‘ 𝑊 ) = ∪ ( TopOpen ‘ 𝑊 ) ) |
14 |
13
|
fveq2d |
⊢ ( 𝑊 ∈ TopSp → ( Moore ‘ ( Base ‘ 𝑊 ) ) = ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ) |
15 |
11 14
|
syl |
⊢ ( 𝑊 ∈ ( TopSp ∩ LMod ) → ( Moore ‘ ( Base ‘ 𝑊 ) ) = ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ) |
16 |
10 15
|
eleqtrd |
⊢ ( 𝑊 ∈ ( TopSp ∩ LMod ) → ( LSubSp ‘ 𝑊 ) ∈ ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ) |
17 |
12
|
tpstop |
⊢ ( 𝑊 ∈ TopSp → ( TopOpen ‘ 𝑊 ) ∈ Top ) |
18 |
|
eqid |
⊢ ∪ ( TopOpen ‘ 𝑊 ) = ∪ ( TopOpen ‘ 𝑊 ) |
19 |
18
|
cldmre |
⊢ ( ( TopOpen ‘ 𝑊 ) ∈ Top → ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ∈ ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ) |
20 |
11 17 19
|
3syl |
⊢ ( 𝑊 ∈ ( TopSp ∩ LMod ) → ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ∈ ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ) |
21 |
|
mreincl |
⊢ ( ( ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ∈ ( Moore ‘ 𝒫 ∪ ( TopOpen ‘ 𝑊 ) ) ∧ ( LSubSp ‘ 𝑊 ) ∈ ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ∧ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ∈ ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ) → ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ∈ ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ) |
22 |
5 16 20 21
|
syl3anc |
⊢ ( 𝑊 ∈ ( TopSp ∩ LMod ) → ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ∈ ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) ) |
23 |
22 1
|
syl |
⊢ ( 𝑊 ∈ ( TopSp ∩ LMod ) → ( toInc ‘ ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ) ∈ CLat ) |