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 = Base I
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