Definition df-llines 34784

Description: Define the set of all "lattice lines" (lattice elements which cover an atom) in a Hilbert lattice k, in other words all elements of height 2 (or lattice dimension 2 or projective dimension 1). (Contributed by NM, 16-Jun-2012.)

Assertion

Ref	Expression
df-llines	|- LLines = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( Atoms ` k ) p ( <o ` k ) x } )

Distinct variable group:   k, p, x

Detailed syntax breakdown of Definition df-llines

Step	Hyp	Ref	Expression
1		clln 34777	. 2 class LLines
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vp	. . . . . . 7 setvar p
5	4	cv 1482	. . . . . 6 class p
6		vx	. . . . . . 7 setvar x
7	6	cv 1482	. . . . . 6 class x
8	2	cv 1482	. . . . . . 7 class k
9		ccvr 34549	. . . . . . 7 class <o
10	8, 9	cfv 5888	. . . . . 6 class ( <o ` k )
11	5, 7, 10	wbr 4653	. . . . 5 wff p ( <o ` k ) x
12		catm 34550	. . . . . 6 class Atoms
13	8, 12	cfv 5888	. . . . 5 class ( Atoms ` k )
14	11, 4, 13	wrex 2913	. . . 4 wff E. p e. ( Atoms ` k ) p ( <o ` k ) x
15		cbs 15857	. . . . 5 class Base
16	8, 15	cfv 5888	. . . 4 class ( Base ` k )
17	14, 6, 16	crab 2916	. . 3 class { x e. ( Base ` k ) | E. p e. ( Atoms ` k ) p ( <o ` k ) x }
18	2, 3, 17	cmpt 4729	. 2 class ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( Atoms ` k ) p ( <o ` k ) x } )
19	1, 18	wceq 1483	1 wff LLines = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( Atoms ` k ) p ( <o ` k ) x } )

This definition is referenced by:  llnset  34791