Metamath Proof Explorer

Theorem mreclatBAD

Description: A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015) TODO ( df-riota update): Reprove using isclat instead of the isclatBAD. hypothesis. See commented-out mreclat above. See mreclat for a good version.

Ref Expression
Hypotheses mreclat.i ⊢I=toInc⁡C
isclatBAD. ⊢I∈CLat↔I∈Poset∧∀xx⊆BaseI→lub⁡I⁡x∈BaseI∧glb⁡I⁡x∈BaseI
Assertion mreclatBAD ⊢C∈Moore⁡X→I∈CLat

Proof

Step Hyp Ref Expression
1 mreclat.i ⊢I=toInc⁡C
2 isclatBAD. ⊢I∈CLat↔I∈Poset∧∀xx⊆BaseI→lub⁡I⁡x∈BaseI∧glb⁡I⁡x∈BaseI
3 1 ipopos ⊢I∈Poset
4 3 a1i ⊢C∈Moore⁡X→I∈Poset
5 eqid ⊢mrCls⁡C=mrCls⁡C
6 eqid ⊢lub⁡I=lub⁡I
7 1 5 6 mrelatlub ⊢C∈Moore⁡X∧x⊆C→lub⁡I⁡x=mrCls⁡C⁡⋃x
8 uniss ⊢x⊆C→⋃x⊆⋃C
9 8 adantl ⊢C∈Moore⁡X∧x⊆C→⋃x⊆⋃C
10 mreuni ⊢C∈Moore⁡X→⋃C=X
11 10 adantr ⊢C∈Moore⁡X∧x⊆C→⋃C=X
12 9 11 sseqtrd ⊢C∈Moore⁡X∧x⊆C→⋃x⊆X
13 5 mrccl ⊢C∈Moore⁡X∧⋃x⊆X→mrCls⁡C⁡⋃x∈C
14 12 13 syldan ⊢C∈Moore⁡X∧x⊆C→mrCls⁡C⁡⋃x∈C
15 7 14 eqeltrd ⊢C∈Moore⁡X∧x⊆C→lub⁡I⁡x∈C
16 fveq2 ⊢x=∅→glb⁡I⁡x=glb⁡I⁡∅
17 16 adantl ⊢C∈Moore⁡X∧x⊆C∧x=∅→glb⁡I⁡x=glb⁡I⁡∅
18 eqid ⊢glb⁡I=glb⁡I
19 1 18 mrelatglb0 ⊢C∈Moore⁡X→glb⁡I⁡∅=X
20 19 ad2antrr ⊢C∈Moore⁡X∧x⊆C∧x=∅→glb⁡I⁡∅=X
21 17 20 eqtrd ⊢C∈Moore⁡X∧x⊆C∧x=∅→glb⁡I⁡x=X
22 mre1cl ⊢C∈Moore⁡X→X∈C
23 22 ad2antrr ⊢C∈Moore⁡X∧x⊆C∧x=∅→X∈C
24 21 23 eqeltrd ⊢C∈Moore⁡X∧x⊆C∧x=∅→glb⁡I⁡x∈C
25 1 18 mrelatglb ⊢C∈Moore⁡X∧x⊆C∧x≠∅→glb⁡I⁡x=⋂x
26 mreintcl ⊢C∈Moore⁡X∧x⊆C∧x≠∅→⋂x∈C
27 25 26 eqeltrd ⊢C∈Moore⁡X∧x⊆C∧x≠∅→glb⁡I⁡x∈C
28 27 3expa ⊢C∈Moore⁡X∧x⊆C∧x≠∅→glb⁡I⁡x∈C
29 24 28 pm2.61dane ⊢C∈Moore⁡X∧x⊆C→glb⁡I⁡x∈C
30 15 29 jca ⊢C∈Moore⁡X∧x⊆C→lub⁡I⁡x∈C∧glb⁡I⁡x∈C
31 30 ex ⊢C∈Moore⁡X→x⊆C→lub⁡I⁡x∈C∧glb⁡I⁡x∈C
32 1 ipobas ⊢C∈Moore⁡X→C=BaseI
33 sseq2 ⊢C=BaseI→x⊆C↔x⊆BaseI
34 eleq2 ⊢C=BaseI→lub⁡I⁡x∈C↔lub⁡I⁡x∈BaseI
35 eleq2 ⊢C=BaseI→glb⁡I⁡x∈C↔glb⁡I⁡x∈BaseI
36 34 35 anbi12d ⊢C=BaseI→lub⁡I⁡x∈C∧glb⁡I⁡x∈C↔lub⁡I⁡x∈BaseI∧glb⁡I⁡x∈BaseI
37 33 36 imbi12d ⊢C=BaseI→x⊆C→lub⁡I⁡x∈C∧glb⁡I⁡x∈C↔x⊆BaseI→lub⁡I⁡x∈BaseI∧glb⁡I⁡x∈BaseI
38 32 37 syl ⊢C∈Moore⁡X→x⊆C→lub⁡I⁡x∈C∧glb⁡I⁡x∈C↔x⊆BaseI→lub⁡I⁡x∈BaseI∧glb⁡I⁡x∈BaseI
39 31 38 mpbid ⊢C∈Moore⁡X→x⊆BaseI→lub⁡I⁡x∈BaseI∧glb⁡I⁡x∈BaseI
40 39 alrimiv ⊢C∈Moore⁡X→∀xx⊆BaseI→lub⁡I⁡x∈BaseI∧glb⁡I⁡x∈BaseI
41 4 40 2 sylanbrc ⊢C∈Moore⁡X→I∈CLat