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 )