Definition df-lplanes

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpl	$$class\mathrm{LPlanes}$$
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		clln	$$class\mathrm{LLines}$$
9	5 8	cfv	$$class\mathrm{LLines}\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{LLines}\left(k\right)p{⋖}_{k}x$$
16	15 3 6	crab	$$class\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{LLines}\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{LLines}\left(k\right)p{⋖}_{k}x\right\}\right)$$
18	0 17	wceq	$$wff\mathrm{LPlanes}=\left(k\in \mathrm{V}⟼\left\{x\in {\mathrm{Base}}_k|\exists p\in \mathrm{LLines}\left(k\right)p{⋖}_{k}x\right\}\right)$$