Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-hlat Structured version   Visualization version   GIF version

Definition df-hlat 34118
Description: Define the class of Hilbert lattices, which are complete, atomic lattices satisfying the superposition principle and minimum height. (Contributed by NM, 5-Nov-2012.)
Assertion
Ref Expression
df-hlat HL = {𝑙 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙))))}
Distinct variable group:   𝑐,𝑙,𝑎,𝑏

Detailed syntax breakdown of Definition df-hlat
StepHypRef Expression
1 chlt 34117 . 2 class HL
2 va . . . . . . . . 9 setvar 𝑎
32cv 1479 . . . . . . . 8 class 𝑎
4 vb . . . . . . . . 9 setvar 𝑏
54cv 1479 . . . . . . . 8 class 𝑏
63, 5wne 2790 . . . . . . 7 wff 𝑎𝑏
7 vc . . . . . . . . . . 11 setvar 𝑐
87cv 1479 . . . . . . . . . 10 class 𝑐
98, 3wne 2790 . . . . . . . . 9 wff 𝑐𝑎
108, 5wne 2790 . . . . . . . . 9 wff 𝑐𝑏
11 vl . . . . . . . . . . . . 13 setvar 𝑙
1211cv 1479 . . . . . . . . . . . 12 class 𝑙
13 cjn 16865 . . . . . . . . . . . 12 class join
1412, 13cfv 5847 . . . . . . . . . . 11 class (join‘𝑙)
153, 5, 14co 6604 . . . . . . . . . 10 class (𝑎(join‘𝑙)𝑏)
16 cple 15869 . . . . . . . . . . 11 class le
1712, 16cfv 5847 . . . . . . . . . 10 class (le‘𝑙)
188, 15, 17wbr 4613 . . . . . . . . 9 wff 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)
199, 10, 18w3a 1036 . . . . . . . 8 wff (𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))
20 catm 34030 . . . . . . . . 9 class Atoms
2112, 20cfv 5847 . . . . . . . 8 class (Atoms‘𝑙)
2219, 7, 21wrex 2908 . . . . . . 7 wff 𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))
236, 22wi 4 . . . . . 6 wff (𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)))
2423, 4, 21wral 2907 . . . . 5 wff 𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)))
2524, 2, 21wral 2907 . . . 4 wff 𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)))
26 cp0 16958 . . . . . . . . . . 11 class 0.
2712, 26cfv 5847 . . . . . . . . . 10 class (0.‘𝑙)
28 cplt 16862 . . . . . . . . . . 11 class lt
2912, 28cfv 5847 . . . . . . . . . 10 class (lt‘𝑙)
3027, 3, 29wbr 4613 . . . . . . . . 9 wff (0.‘𝑙)(lt‘𝑙)𝑎
313, 5, 29wbr 4613 . . . . . . . . 9 wff 𝑎(lt‘𝑙)𝑏
3230, 31wa 384 . . . . . . . 8 wff ((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏)
335, 8, 29wbr 4613 . . . . . . . . 9 wff 𝑏(lt‘𝑙)𝑐
34 cp1 16959 . . . . . . . . . . 11 class 1.
3512, 34cfv 5847 . . . . . . . . . 10 class (1.‘𝑙)
368, 35, 29wbr 4613 . . . . . . . . 9 wff 𝑐(lt‘𝑙)(1.‘𝑙)
3733, 36wa 384 . . . . . . . 8 wff (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙))
3832, 37wa 384 . . . . . . 7 wff (((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙)))
39 cbs 15781 . . . . . . . 8 class Base
4012, 39cfv 5847 . . . . . . 7 class (Base‘𝑙)
4138, 7, 40wrex 2908 . . . . . 6 wff 𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙)))
4241, 4, 40wrex 2908 . . . . 5 wff 𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙)))
4342, 2, 40wrex 2908 . . . 4 wff 𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙)))
4425, 43wa 384 . . 3 wff (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙))))
45 coml 33942 . . . . 5 class OML
46 ccla 17028 . . . . 5 class CLat
4745, 46cin 3554 . . . 4 class (OML ∩ CLat)
48 clc 34032 . . . 4 class CvLat
4947, 48cin 3554 . . 3 class ((OML ∩ CLat) ∩ CvLat)
5044, 11, 49crab 2911 . 2 class {𝑙 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙))))}
511, 50wceq 1480 1 wff HL = {𝑙 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙))))}
Colors of variables: wff setvar class
This definition is referenced by:  ishlat1  34119
  Copyright terms: Public domain W3C validator