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 )