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	⊢ LPlanes = ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clpl	⊢ LPlanes
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑘
6	5 4	cfv	⊢ ( Base ‘ 𝑘 )
7		vp	⊢ 𝑝
8		clln	⊢ LLines
9	5 8	cfv	⊢ ( LLines ‘ 𝑘 )
10	7	cv	⊢ 𝑝
11		ccvr	⊢ ⋖
12	5 11	cfv	⊢ ( ⋖ ‘ 𝑘 )
13	3	cv	⊢ 𝑥
14	10 13 12	wbr	⊢ 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥
15	14 7 9	wrex	⊢ ∃ 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥
16	15 3 6	crab	⊢ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 }
17	1 2 16	cmpt	⊢ ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )
18	0 17	wceq	⊢ LPlanes = ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( LLines ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )