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 e. CLat <-> ( I e. Poset /\ A. x ( x C_ ( Base ` I ) -> ( ( ( lub ` I ) ` x ) e. ( Base ` I ) /\ ( ( glb ` I ) ` x ) e. ( Base ` I ) ) ) ) )
Assertion mreclatBAD 
|- ( C e. ( Moore ` X ) -> I e. CLat )

Proof

Step Hyp Ref Expression
1 mreclat.i 
 |-  I = ( toInc ` C )
2 isclatBAD. 
 |-  ( I e. CLat <-> ( I e. Poset /\ A. x ( x C_ ( Base ` I ) -> ( ( ( lub ` I ) ` x ) e. ( Base ` I ) /\ ( ( glb ` I ) ` x ) e. ( Base ` I ) ) ) ) )
3 1 ipopos 
 |-  I e. Poset
4 3 a1i 
 |-  ( C e. ( Moore ` X ) -> I e. Poset )
5 eqid 
 |-  ( mrCls ` C ) = ( mrCls ` C )
6 eqid 
 |-  ( lub ` I ) = ( lub ` I )
7 1 5 6 mrelatlub 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( ( lub ` I ) ` x ) = ( ( mrCls ` C ) ` U. x ) )
8 uniss 
 |-  ( x C_ C -> U. x C_ U. C )
9 8 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> U. x C_ U. C )
10 mreuni 
 |-  ( C e. ( Moore ` X ) -> U. C = X )
11 10 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> U. C = X )
12 9 11 sseqtrd 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> U. x C_ X )
13 5 mrccl 
 |-  ( ( C e. ( Moore ` X ) /\ U. x C_ X ) -> ( ( mrCls ` C ) ` U. x ) e. C )
14 12 13 syldan 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( ( mrCls ` C ) ` U. x ) e. C )
15 7 14 eqeltrd 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( ( lub ` I ) ` x ) e. C )
16 fveq2 
 |-  ( x = (/) -> ( ( glb ` I ) ` x ) = ( ( glb ` I ) ` (/) ) )
17 16 adantl 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) -> ( ( glb ` I ) ` x ) = ( ( glb ` I ) ` (/) ) )
18 eqid 
 |-  ( glb ` I ) = ( glb ` I )
19 1 18 mrelatglb0 
 |-  ( C e. ( Moore ` X ) -> ( ( glb ` I ) ` (/) ) = X )
20 19 ad2antrr 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) -> ( ( glb ` I ) ` (/) ) = X )
21 17 20 eqtrd 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) -> ( ( glb ` I ) ` x ) = X )
22 mre1cl 
 |-  ( C e. ( Moore ` X ) -> X e. C )
23 22 ad2antrr 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) -> X e. C )
24 21 23 eqeltrd 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) -> ( ( glb ` I ) ` x ) e. C )
25 1 18 mrelatglb 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C /\ x =/= (/) ) -> ( ( glb ` I ) ` x ) = |^| x )
26 mreintcl 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C /\ x =/= (/) ) -> |^| x e. C )
27 25 26 eqeltrd 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C /\ x =/= (/) ) -> ( ( glb ` I ) ` x ) e. C )
28 27 3expa 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x =/= (/) ) -> ( ( glb ` I ) ` x ) e. C )
29 24 28 pm2.61dane 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( ( glb ` I ) ` x ) e. C )
30 15 29 jca 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( ( ( lub ` I ) ` x ) e. C /\ ( ( glb ` I ) ` x ) e. C ) )
31 30 ex 
 |-  ( C e. ( Moore ` X ) -> ( x C_ C -> ( ( ( lub ` I ) ` x ) e. C /\ ( ( glb ` I ) ` x ) e. C ) ) )
32 1 ipobas 
 |-  ( C e. ( Moore ` X ) -> C = ( Base ` I ) )
33 sseq2 
 |-  ( C = ( Base ` I ) -> ( x C_ C <-> x C_ ( Base ` I ) ) )
34 eleq2 
 |-  ( C = ( Base ` I ) -> ( ( ( lub ` I ) ` x ) e. C <-> ( ( lub ` I ) ` x ) e. ( Base ` I ) ) )
35 eleq2 
 |-  ( C = ( Base ` I ) -> ( ( ( glb ` I ) ` x ) e. C <-> ( ( glb ` I ) ` x ) e. ( Base ` I ) ) )
36 34 35 anbi12d 
 |-  ( C = ( Base ` I ) -> ( ( ( ( lub ` I ) ` x ) e. C /\ ( ( glb ` I ) ` x ) e. C ) <-> ( ( ( lub ` I ) ` x ) e. ( Base ` I ) /\ ( ( glb ` I ) ` x ) e. ( Base ` I ) ) ) )
37 33 36 imbi12d 
 |-  ( C = ( Base ` I ) -> ( ( x C_ C -> ( ( ( lub ` I ) ` x ) e. C /\ ( ( glb ` I ) ` x ) e. C ) ) <-> ( x C_ ( Base ` I ) -> ( ( ( lub ` I ) ` x ) e. ( Base ` I ) /\ ( ( glb ` I ) ` x ) e. ( Base ` I ) ) ) ) )
38 32 37 syl 
 |-  ( C e. ( Moore ` X ) -> ( ( x C_ C -> ( ( ( lub ` I ) ` x ) e. C /\ ( ( glb ` I ) ` x ) e. C ) ) <-> ( x C_ ( Base ` I ) -> ( ( ( lub ` I ) ` x ) e. ( Base ` I ) /\ ( ( glb ` I ) ` x ) e. ( Base ` I ) ) ) ) )
39 31 38 mpbid 
 |-  ( C e. ( Moore ` X ) -> ( x C_ ( Base ` I ) -> ( ( ( lub ` I ) ` x ) e. ( Base ` I ) /\ ( ( glb ` I ) ` x ) e. ( Base ` I ) ) ) )
40 39 alrimiv 
 |-  ( C e. ( Moore ` X ) -> A. x ( x C_ ( Base ` I ) -> ( ( ( lub ` I ) ` x ) e. ( Base ` I ) /\ ( ( glb ` I ) ` x ) e. ( Base ` I ) ) ) )
41 4 40 2 sylanbrc 
 |-  ( C e. ( Moore ` X ) -> I e. CLat )