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.

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

Proof

Step Hyp Ref Expression
1 mreclat.i ⊢ I = toInc ⁡ C
2 isclatBAD. ⊢ I ∈ CLat ↔ I ∈ Poset ∧ ∀ x x ⊆ Base I → lub ⁡ I ⁡ x ∈ Base I ∧ glb ⁡ I ⁡ x ∈ Base I
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 = Base I
33 sseq2 ⊢ C = Base I → x ⊆ C ↔ x ⊆ Base I
34 eleq2 ⊢ C = Base I → lub ⁡ I ⁡ x ∈ C ↔ lub ⁡ I ⁡ x ∈ Base I
35 eleq2 ⊢ C = Base I → glb ⁡ I ⁡ x ∈ C ↔ glb ⁡ I ⁡ x ∈ Base I
36 34 35 anbi12d ⊢ C = Base I → lub ⁡ I ⁡ x ∈ C ∧ glb ⁡ I ⁡ x ∈ C ↔ lub ⁡ I ⁡ x ∈ Base I ∧ glb ⁡ I ⁡ x ∈ Base I
37 33 36 imbi12d ⊢ C = Base I → x ⊆ C → lub ⁡ I ⁡ x ∈ C ∧ glb ⁡ I ⁡ x ∈ C ↔ x ⊆ Base I → lub ⁡ I ⁡ x ∈ Base I ∧ glb ⁡ I ⁡ x ∈ Base I
38 32 37 syl ⊢ C ∈ Moore ⁡ X → x ⊆ C → lub ⁡ I ⁡ x ∈ C ∧ glb ⁡ I ⁡ x ∈ C ↔ x ⊆ Base I → lub ⁡ I ⁡ x ∈ Base I ∧ glb ⁡ I ⁡ x ∈ Base I
39 31 38 mpbid ⊢ C ∈ Moore ⁡ X → x ⊆ Base I → lub ⁡ I ⁡ x ∈ Base I ∧ glb ⁡ I ⁡ x ∈ Base I
40 39 alrimiv ⊢ C ∈ Moore ⁡ X → ∀ x x ⊆ Base I → lub ⁡ I ⁡ x ∈ Base I ∧ glb ⁡ I ⁡ x ∈ Base I
41 4 40 2 sylanbrc ⊢ C ∈ Moore ⁡ X → I ∈ CLat