Metamath Proof Explorer


Definition df-hlat

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)

Ref Expression
Assertion df-hlat
|- HL = { l e. ( ( OML i^i CLat ) i^i CvLat ) | ( A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) /\ E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 chlt
 |-  HL
1 vl
 |-  l
2 coml
 |-  OML
3 ccla
 |-  CLat
4 2 3 cin
 |-  ( OML i^i CLat )
5 clc
 |-  CvLat
6 4 5 cin
 |-  ( ( OML i^i CLat ) i^i CvLat )
7 va
 |-  a
8 catm
 |-  Atoms
9 1 cv
 |-  l
10 9 8 cfv
 |-  ( Atoms ` l )
11 vb
 |-  b
12 7 cv
 |-  a
13 11 cv
 |-  b
14 12 13 wne
 |-  a =/= b
15 vc
 |-  c
16 15 cv
 |-  c
17 16 12 wne
 |-  c =/= a
18 16 13 wne
 |-  c =/= b
19 cple
 |-  le
20 9 19 cfv
 |-  ( le ` l )
21 cjn
 |-  join
22 9 21 cfv
 |-  ( join ` l )
23 12 13 22 co
 |-  ( a ( join ` l ) b )
24 16 23 20 wbr
 |-  c ( le ` l ) ( a ( join ` l ) b )
25 17 18 24 w3a
 |-  ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) )
26 25 15 10 wrex
 |-  E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) )
27 14 26 wi
 |-  ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) )
28 27 11 10 wral
 |-  A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) )
29 28 7 10 wral
 |-  A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) )
30 cbs
 |-  Base
31 9 30 cfv
 |-  ( Base ` l )
32 cp0
 |-  0.
33 9 32 cfv
 |-  ( 0. ` l )
34 cplt
 |-  lt
35 9 34 cfv
 |-  ( lt ` l )
36 33 12 35 wbr
 |-  ( 0. ` l ) ( lt ` l ) a
37 12 13 35 wbr
 |-  a ( lt ` l ) b
38 36 37 wa
 |-  ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b )
39 13 16 35 wbr
 |-  b ( lt ` l ) c
40 cp1
 |-  1.
41 9 40 cfv
 |-  ( 1. ` l )
42 16 41 35 wbr
 |-  c ( lt ` l ) ( 1. ` l )
43 39 42 wa
 |-  ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) )
44 38 43 wa
 |-  ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) )
45 44 15 31 wrex
 |-  E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) )
46 45 11 31 wrex
 |-  E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) )
47 46 7 31 wrex
 |-  E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) )
48 29 47 wa
 |-  ( A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) /\ E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) )
49 48 1 6 crab
 |-  { l e. ( ( OML i^i CLat ) i^i CvLat ) | ( A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) /\ E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) ) }
50 0 49 wceq
 |-  HL = { l e. ( ( OML i^i CLat ) i^i CvLat ) | ( A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) /\ E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) ) }