Metamath Proof Explorer


Theorem mreclatdemoBAD

Description: The closed subspaces of a topology-bearing module form a complete lattice. Demonstration for mreclatBAD . (Contributed by Stefan O'Rear, 31-Jan-2015) TODO ( df-riota update): This proof uses the old df-clat and references the required instance of mreclatBAD as a hypothesis. When mreclatBAD is corrected to become mreclat, delete this theorem and uncomment the mreclatdemo below.

Ref Expression
Hypothesis mreclatBAD. LSubSp W Clsd TopOpen W Moore TopOpen W toInc LSubSp W Clsd TopOpen W CLat
Assertion mreclatdemoBAD W TopSp LMod toInc LSubSp W Clsd TopOpen W CLat

Proof

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