Definition df-lplanes 29981

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 29974	. 2 class LPlanes
2		vk	. . 3 set k
3		cvv 2916	. . 3 class _V
4		vp	. . . . . . 7 set p
5	4	cv 1648	. . . . . 6 class p
6		vx	. . . . . . 7 set x
7	6	cv 1648	. . . . . 6 class x
8	2	cv 1648	. . . . . . 7 class k
9		ccvr 29745	. . . . . . 7 class <o
10	8, 9	cfv 5413	. . . . . 6 class ( <o ` k )
11	5, 7, 10	wbr 4172	. . . . 5 wff p ( <o ` k ) x
12		clln 29973	. . . . . 6 class LLines
13	8, 12	cfv 5413	. . . . 5 class ( LLines ` k )
14	11, 4, 13	wrex 2667	. . . 4 wff E. p e. ( LLines ` k ) p ( <o ` k ) x
15		cbs 13424	. . . . 5 class Base
16	8, 15	cfv 5413	. . . 4 class ( Base ` k )
17	14, 6, 16	crab 2670	. . 3 class { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( <o ` k ) x }
18	2, 3, 17	cmpt 4226	. 2 class ( k e. _V |-> { x e. ( Base ` k ) | E. p e. ( LLines ` k ) p ( <o ` k ) x } )
19	1, 18	wceq 1649	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  30011