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. LSubSpWClsdTopOpenWMooreTopOpenWtoIncLSubSpWClsdTopOpenWCLat
Assertion mreclatdemoBAD WTopSpLModtoIncLSubSpWClsdTopOpenWCLat

Proof

Step Hyp Ref Expression
1 mreclatBAD. LSubSpWClsdTopOpenWMooreTopOpenWtoIncLSubSpWClsdTopOpenWCLat
2 fvex TopOpenWV
3 2 uniex TopOpenWV
4 mremre TopOpenWVMooreTopOpenWMoore𝒫TopOpenW
5 3 4 mp1i WTopSpLModMooreTopOpenWMoore𝒫TopOpenW
6 elinel2 WTopSpLModWLMod
7 eqid BaseW=BaseW
8 eqid LSubSpW=LSubSpW
9 7 8 lssmre WLModLSubSpWMooreBaseW
10 6 9 syl WTopSpLModLSubSpWMooreBaseW
11 elinel1 WTopSpLModWTopSp
12 eqid TopOpenW=TopOpenW
13 7 12 tpsuni WTopSpBaseW=TopOpenW
14 13 fveq2d WTopSpMooreBaseW=MooreTopOpenW
15 11 14 syl WTopSpLModMooreBaseW=MooreTopOpenW
16 10 15 eleqtrd WTopSpLModLSubSpWMooreTopOpenW
17 12 tpstop WTopSpTopOpenWTop
18 eqid TopOpenW=TopOpenW
19 18 cldmre TopOpenWTopClsdTopOpenWMooreTopOpenW
20 11 17 19 3syl WTopSpLModClsdTopOpenWMooreTopOpenW
21 mreincl MooreTopOpenWMoore𝒫TopOpenWLSubSpWMooreTopOpenWClsdTopOpenWMooreTopOpenWLSubSpWClsdTopOpenWMooreTopOpenW
22 5 16 20 21 syl3anc WTopSpLModLSubSpWClsdTopOpenWMooreTopOpenW
23 22 1 syl WTopSpLModtoIncLSubSpWClsdTopOpenWCLat