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 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