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 ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ∈ ( Moore ‘ ∪ ( TopOpen ‘ 𝑊 ) ) → ( toInc ‘ ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ) ∈ CLat )
Assertion mreclatdemoBAD ( 𝑊 ∈ ( TopSp ∩ LMod ) → ( toInc ‘ ( ( LSubSp ‘ 𝑊 ) ∩ ( Clsd ‘ ( TopOpen ‘ 𝑊 ) ) ) ) ∈ CLat )

Proof

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 )