This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )