Definition df-hlat 34638

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

Distinct variable group:   c, l, a, b

Detailed syntax breakdown of Definition df-hlat

Step	Hyp	Ref	Expression
1		chlt 34637	. 2 class HL
2		va	. . . . . . . . 9 setvar a
3	2	cv 1482	. . . . . . . 8 class a
4		vb	. . . . . . . . 9 setvar b
5	4	cv 1482	. . . . . . . 8 class b
6	3, 5	wne 2794	. . . . . . 7 wff a =/= b
7		vc	. . . . . . . . . . 11 setvar c
8	7	cv 1482	. . . . . . . . . 10 class c
9	8, 3	wne 2794	. . . . . . . . 9 wff c =/= a
10	8, 5	wne 2794	. . . . . . . . 9 wff c =/= b
11		vl	. . . . . . . . . . . . 13 setvar l
12	11	cv 1482	. . . . . . . . . . . 12 class l
13		cjn 16944	. . . . . . . . . . . 12 class join
14	12, 13	cfv 5888	. . . . . . . . . . 11 class ( join ` l )
15	3, 5, 14	co 6650	. . . . . . . . . 10 class ( a ( join ` l ) b )
16		cple 15948	. . . . . . . . . . 11 class le
17	12, 16	cfv 5888	. . . . . . . . . 10 class ( le ` l )
18	8, 15, 17	wbr 4653	. . . . . . . . 9 wff c ( le ` l ) ( a ( join ` l ) b )
19	9, 10, 18	w3a 1037	. . . . . . . 8 wff ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) )
20		catm 34550	. . . . . . . . 9 class Atoms
21	12, 20	cfv 5888	. . . . . . . 8 class ( Atoms ` l )
22	19, 7, 21	wrex 2913	. . . . . . 7 wff E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) )
23	6, 22	wi 4	. . . . . 6 wff ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) )
24	23, 4, 21	wral 2912	. . . . 5 wff A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) )
25	24, 2, 21	wral 2912	. . . 4 wff 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 ) ) )
26		cp0 17037	. . . . . . . . . . 11 class 0.
27	12, 26	cfv 5888	. . . . . . . . . 10 class ( 0. ` l )
28		cplt 16941	. . . . . . . . . . 11 class lt
29	12, 28	cfv 5888	. . . . . . . . . 10 class ( lt ` l )
30	27, 3, 29	wbr 4653	. . . . . . . . 9 wff ( 0. ` l ) ( lt ` l ) a
31	3, 5, 29	wbr 4653	. . . . . . . . 9 wff a ( lt ` l ) b
32	30, 31	wa 384	. . . . . . . 8 wff ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b )
33	5, 8, 29	wbr 4653	. . . . . . . . 9 wff b ( lt ` l ) c
34		cp1 17038	. . . . . . . . . . 11 class 1.
35	12, 34	cfv 5888	. . . . . . . . . 10 class ( 1. ` l )
36	8, 35, 29	wbr 4653	. . . . . . . . 9 wff c ( lt ` l ) ( 1. ` l )
37	33, 36	wa 384	. . . . . . . 8 wff ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) )
38	32, 37	wa 384	. . . . . . 7 wff ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) )
39		cbs 15857	. . . . . . . 8 class Base
40	12, 39	cfv 5888	. . . . . . 7 class ( Base ` l )
41	38, 7, 40	wrex 2913	. . . . . 6 wff E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) )
42	41, 4, 40	wrex 2913	. . . . 5 wff 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 ) ) )
43	42, 2, 40	wrex 2913	. . . 4 wff 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 ) ) )
44	25, 43	wa 384	. . 3 wff ( 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 ) ) ) )
45		coml 34462	. . . . 5 class OML
46		ccla 17107	. . . . 5 class CLat
47	45, 46	cin 3573	. . . 4 class ( OML i^i CLat )
48		clc 34552	. . . 4 class CvLat
49	47, 48	cin 3573	. . 3 class ( ( OML i^i CLat ) i^i CvLat )
50	44, 11, 49	crab 2916	. 2 class { 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 ) ) ) ) }
51	1, 50	wceq 1483	1 wff 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 ) ) ) ) }

This definition is referenced by:  ishlat1  34639