Metamath Proof Explorer

Theorem mreclat

Description: A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024)

Ref Expression
Hypothesis mreclatGOOD.i ⊢I=toInc⁡C
Assertion mreclat ⊢C∈Moore⁡X→I∈CLat

Proof

Step Hyp Ref Expression
1 mreclatGOOD.i ⊢I=toInc⁡C
2 1 ipobas ⊢C∈Moore⁡X→C=BaseI
3 eqidd ⊢C∈Moore⁡X→lub⁡I=lub⁡I
4 eqidd ⊢C∈Moore⁡X→glb⁡I=glb⁡I
5 1 ipopos ⊢I∈Poset
6 5 a1i ⊢C∈Moore⁡X→I∈Poset
7 mreuniss ⊢C∈Moore⁡X∧x⊆C→⋃x⊆X
8 eqid ⊢mrCls⁡C=mrCls⁡C
9 8 mrccl ⊢C∈Moore⁡X∧⋃x⊆X→mrCls⁡C⁡⋃x∈C
10 7 9 syldan ⊢C∈Moore⁡X∧x⊆C→mrCls⁡C⁡⋃x∈C
11 simpl ⊢C∈Moore⁡X∧x⊆C→C∈Moore⁡X
12 simpr ⊢C∈Moore⁡X∧x⊆C→x⊆C
13 eqidd ⊢C∈Moore⁡X∧x⊆C→lub⁡I=lub⁡I
14 8 mrcval ⊢C∈Moore⁡X∧⋃x⊆X→mrCls⁡C⁡⋃x=⋂y∈C|⋃x⊆y
15 7 14 syldan ⊢C∈Moore⁡X∧x⊆C→mrCls⁡C⁡⋃x=⋂y∈C|⋃x⊆y
16 1 11 12 13 15 ipolubdm ⊢C∈Moore⁡X∧x⊆C→x∈dom⁡lub⁡I↔mrCls⁡C⁡⋃x∈C
17 10 16 mpbird ⊢C∈Moore⁡X∧x⊆C→x∈dom⁡lub⁡I
18 ssv ⊢y⊆V
19 int0 ⊢⋂∅=V
20 18 19 sseqtrri ⊢y⊆⋂∅
21 simplr ⊢C∈Moore⁡X∧x⊆C∧x=∅∧y∈C→x=∅
22 21 inteqd ⊢C∈Moore⁡X∧x⊆C∧x=∅∧y∈C→⋂x=⋂∅
23 20 22 sseqtrrid ⊢C∈Moore⁡X∧x⊆C∧x=∅∧y∈C→y⊆⋂x
24 23 rabeqcda ⊢C∈Moore⁡X∧x⊆C∧x=∅→y∈C|y⊆⋂x=C
25 24 unieqd ⊢C∈Moore⁡X∧x⊆C∧x=∅→⋃y∈C|y⊆⋂x=⋃C
26 mreuni ⊢C∈Moore⁡X→⋃C=X
27 mre1cl ⊢C∈Moore⁡X→X∈C
28 26 27 eqeltrd ⊢C∈Moore⁡X→⋃C∈C
29 28 ad2antrr ⊢C∈Moore⁡X∧x⊆C∧x=∅→⋃C∈C
30 25 29 eqeltrd ⊢C∈Moore⁡X∧x⊆C∧x=∅→⋃y∈C|y⊆⋂x∈C
31 mreintcl ⊢C∈Moore⁡X∧x⊆C∧x≠∅→⋂x∈C
32 unimax ⊢⋂x∈C→⋃y∈C|y⊆⋂x=⋂x
33 31 32 syl ⊢C∈Moore⁡X∧x⊆C∧x≠∅→⋃y∈C|y⊆⋂x=⋂x
34 33 31 eqeltrd ⊢C∈Moore⁡X∧x⊆C∧x≠∅→⋃y∈C|y⊆⋂x∈C
35 34 3expa ⊢C∈Moore⁡X∧x⊆C∧x≠∅→⋃y∈C|y⊆⋂x∈C
36 30 35 pm2.61dane ⊢C∈Moore⁡X∧x⊆C→⋃y∈C|y⊆⋂x∈C
37 eqidd ⊢C∈Moore⁡X∧x⊆C→glb⁡I=glb⁡I
38 eqidd ⊢C∈Moore⁡X∧x⊆C→⋃y∈C|y⊆⋂x=⋃y∈C|y⊆⋂x
39 1 11 12 37 38 ipoglbdm ⊢C∈Moore⁡X∧x⊆C→x∈dom⁡glb⁡I↔⋃y∈C|y⊆⋂x∈C
40 36 39 mpbird ⊢C∈Moore⁡X∧x⊆C→x∈dom⁡glb⁡I
41 2 3 4 6 17 40 isclatd ⊢C∈Moore⁡X→I∈CLat