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 35110
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 35109 . 2 class HL
2 va . . . . . . . . 9 setvar 𝑎
32cv 1619 . . . . . . . 8 class 𝑎
4 vb . . . . . . . . 9 setvar 𝑏
54cv 1619 . . . . . . . 8 class 𝑏
63, 5wne 2920 . . . . . . 7 wff 𝑎𝑏
7 vc . . . . . . . . . . 11 setvar 𝑐
87cv 1619 . . . . . . . . . 10 class 𝑐
98, 3wne 2920 . . . . . . . . 9 wff 𝑐𝑎
108, 5wne 2920 . . . . . . . . 9 wff 𝑐𝑏
11 vl . . . . . . . . . . . . 13 setvar 𝑙
1211cv 1619 . . . . . . . . . . . 12 class 𝑙
13 cjn 17116 . . . . . . . . . . . 12 class join
1412, 13cfv 6037 . . . . . . . . . . 11 class (join‘𝑙)
153, 5, 14co 6801 . . . . . . . . . 10 class (𝑎(join‘𝑙)𝑏)
16 cple 16121 . . . . . . . . . . 11 class le
1712, 16cfv 6037 . . . . . . . . . 10 class (le‘𝑙)
188, 15, 17wbr 4792 . . . . . . . . 9 wff 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)
199, 10, 18w3a 1072 . . . . . . . 8 wff (𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))
20 catm 35022 . . . . . . . . 9 class Atoms
2112, 20cfv 6037 . . . . . . . 8 class (Atoms‘𝑙)
2219, 7, 21wrex 3039 . . . . . . 7 wff 𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))
236, 22wi 4 . . . . . 6 wff (𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)))
2423, 4, 21wral 3038 . . . . 5 wff 𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)))
2524, 2, 21wral 3038 . . . 4 wff 𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏)))
26 cp0 17209 . . . . . . . . . . 11 class 0.
2712, 26cfv 6037 . . . . . . . . . 10 class (0.‘𝑙)
28 cplt 17113 . . . . . . . . . . 11 class lt
2912, 28cfv 6037 . . . . . . . . . 10 class (lt‘𝑙)
3027, 3, 29wbr 4792 . . . . . . . . 9 wff (0.‘𝑙)(lt‘𝑙)𝑎
313, 5, 29wbr 4792 . . . . . . . . 9 wff 𝑎(lt‘𝑙)𝑏
3230, 31wa 383 . . . . . . . 8 wff ((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏)
335, 8, 29wbr 4792 . . . . . . . . 9 wff 𝑏(lt‘𝑙)𝑐
34 cp1 17210 . . . . . . . . . . 11 class 1.
3512, 34cfv 6037 . . . . . . . . . 10 class (1.‘𝑙)
368, 35, 29wbr 4792 . . . . . . . . 9 wff 𝑐(lt‘𝑙)(1.‘𝑙)
3733, 36wa 383 . . . . . . . 8 wff (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙))
3832, 37wa 383 . . . . . . 7 wff (((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙)))
39 cbs 16030 . . . . . . . 8 class Base
4012, 39cfv 6037 . . . . . . 7 class (Base‘𝑙)
4138, 7, 40wrex 3039 . . . . . 6 wff 𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙)))
4241, 4, 40wrex 3039 . . . . 5 wff 𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙)))
4342, 2, 40wrex 3039 . . . 4 wff 𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙)))
4425, 43wa 383 . . 3 wff (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙))))
45 coml 34934 . . . . 5 class OML
46 ccla 17279 . . . . 5 class CLat
4745, 46cin 3702 . . . 4 class (OML ∩ CLat)
48 clc 35024 . . . 4 class CvLat
4947, 48cin 3702 . . 3 class ((OML ∩ CLat) ∩ CvLat)
5044, 11, 49crab 3042 . 2 class {𝑙 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐𝑎𝑐𝑏𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐𝑐(lt‘𝑙)(1.‘𝑙))))}
511, 50wceq 1620 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  35111
  Copyright terms: Public domain W3C validator