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 ) i^i ( Clsd ` ( TopOpen ` W ) ) ) e. ( Moore ` U. ( TopOpen ` W ) ) -> ( toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat )
Assertion mreclatdemoBAD
|- ( W e. ( TopSp i^i LMod ) -> ( toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat )

Proof

Step Hyp Ref Expression
1 mreclatBAD.
 |-  ( ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) e. ( Moore ` U. ( TopOpen ` W ) ) -> ( toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat )
2 fvex
 |-  ( TopOpen ` W ) e. _V
3 2 uniex
 |-  U. ( TopOpen ` W ) e. _V
4 mremre
 |-  ( U. ( TopOpen ` W ) e. _V -> ( Moore ` U. ( TopOpen ` W ) ) e. ( Moore ` ~P U. ( TopOpen ` W ) ) )
5 3 4 mp1i
 |-  ( W e. ( TopSp i^i LMod ) -> ( Moore ` U. ( TopOpen ` W ) ) e. ( Moore ` ~P U. ( TopOpen ` W ) ) )
6 elinel2
 |-  ( W e. ( TopSp i^i LMod ) -> W e. LMod )
7 eqid
 |-  ( Base ` W ) = ( Base ` W )
8 eqid
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 7 8 lssmre
 |-  ( W e. LMod -> ( LSubSp ` W ) e. ( Moore ` ( Base ` W ) ) )
10 6 9 syl
 |-  ( W e. ( TopSp i^i LMod ) -> ( LSubSp ` W ) e. ( Moore ` ( Base ` W ) ) )
11 elinel1
 |-  ( W e. ( TopSp i^i LMod ) -> W e. TopSp )
12 eqid
 |-  ( TopOpen ` W ) = ( TopOpen ` W )
13 7 12 tpsuni
 |-  ( W e. TopSp -> ( Base ` W ) = U. ( TopOpen ` W ) )
14 13 fveq2d
 |-  ( W e. TopSp -> ( Moore ` ( Base ` W ) ) = ( Moore ` U. ( TopOpen ` W ) ) )
15 11 14 syl
 |-  ( W e. ( TopSp i^i LMod ) -> ( Moore ` ( Base ` W ) ) = ( Moore ` U. ( TopOpen ` W ) ) )
16 10 15 eleqtrd
 |-  ( W e. ( TopSp i^i LMod ) -> ( LSubSp ` W ) e. ( Moore ` U. ( TopOpen ` W ) ) )
17 12 tpstop
 |-  ( W e. TopSp -> ( TopOpen ` W ) e. Top )
18 eqid
 |-  U. ( TopOpen ` W ) = U. ( TopOpen ` W )
19 18 cldmre
 |-  ( ( TopOpen ` W ) e. Top -> ( Clsd ` ( TopOpen ` W ) ) e. ( Moore ` U. ( TopOpen ` W ) ) )
20 11 17 19 3syl
 |-  ( W e. ( TopSp i^i LMod ) -> ( Clsd ` ( TopOpen ` W ) ) e. ( Moore ` U. ( TopOpen ` W ) ) )
21 mreincl
 |-  ( ( ( Moore ` U. ( TopOpen ` W ) ) e. ( Moore ` ~P U. ( TopOpen ` W ) ) /\ ( LSubSp ` W ) e. ( Moore ` U. ( TopOpen ` W ) ) /\ ( Clsd ` ( TopOpen ` W ) ) e. ( Moore ` U. ( TopOpen ` W ) ) ) -> ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) e. ( Moore ` U. ( TopOpen ` W ) ) )
22 5 16 20 21 syl3anc
 |-  ( W e. ( TopSp i^i LMod ) -> ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) e. ( Moore ` U. ( TopOpen ` W ) ) )
23 22 1 syl
 |-  ( W e. ( TopSp i^i LMod ) -> ( toInc ` ( ( LSubSp ` W ) i^i ( Clsd ` ( TopOpen ` W ) ) ) ) e. CLat )