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