Definition df-llines

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)

	Ref	Expression
Assertion	df-llines	$$⊢\mathrm{LLines}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{Atoms}\left(k\right)p{⋖}_{k}x\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clln	$$class\mathrm{LLines}$$
1		vk	$$setvark$$
2		cvv	$$class\mathrm{V}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvark$$
6	5 4	cfv	$$class{\mathrm{Base}}_k$$
7		vp	$$setvarp$$
8		catm	$$class\mathrm{Atoms}$$
9	5 8	cfv	$$class\mathrm{Atoms}\left(k\right)$$
10	7	cv	$$setvarp$$
11		ccvr	$$class⋖$$
12	5 11	cfv	$$class{⋖}_k$$
13	3	cv	$$setvarx$$
14	10 13 12	wbr	$$wffp{⋖}_{k}x$$
15	14 7 9	wrex	$$wff\exists p\in \mathrm{Atoms}\left(k\right)p{⋖}_{k}x$$
16	15 3 6	crab	$$class\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{Atoms}\left(k\right)p{⋖}_{k}x\right\}$$
17	1 2 16	cmpt	$$class\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{Atoms}\left(k\right)p{⋖}_{k}x\right\}\right)$$
18	0 17	wceq	$$wff\mathrm{LLines}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{Atoms}\left(k\right)p{⋖}_{k}x\right\}\right)$$