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