Definition df-lplanes 33033

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

Assertion

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

Distinct variable group:   k, p, x

Detailed syntax breakdown of Definition df-lplanes

Step	Hyp	Ref	Expression
1		clpl 33026	. 2 class LPlanes
2		vk	. . 3 setvar k
3		cvv 3080	. . 3 class _V
4		vp	. . . . . . 7 setvar p
5	4	cv 1436	. . . . . 6 class p
6		vx	. . . . . . 7 setvar x
7	6	cv 1436	. . . . . 6 class x
8	2	cv 1436	. . . . . . 7 class k
9		ccvr 32797	. . . . . . 7 class <o
10	8, 9	cfv 5601	. . . . . 6 class ( <o ` k )
11	5, 7, 10	wbr 4423	. . . . 5 wff p ( <o ` k ) x
12		clln 33025	. . . . . 6 class LLines
13	8, 12	cfv 5601	. . . . 5 class ( LLines ` k )
14	11, 4, 13	wrex 2772	. . . 4 wff E. p e. ( LLines ` k ) p ( <o ` k ) x
15		cbs 15120	. . . . 5 class Base
16	8, 15	cfv 5601	. . . 4 class ( Base ` k )
17	14, 6, 16	crab 2775	. . 3 class { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( <o ` k ) x }
18	2, 3, 17	cmpt 4482	. 2 class ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( <o ` k ) x } )
19	1, 18	wceq 1437	1 wff LPlanes = ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( <o ` k ) x } )

This definition is referenced by:  lplnset  33063