Definition df-lvols

Description: Define the set of all 3-dimensional "lattice volumes" (lattice elements which cover a plane) in a Hilbert lattice k , in other words all elements of height 4 (or lattice dimension 4 or projective dimension 3). (Contributed by NM, 1-Jul-2012)

	Ref	Expression
Assertion	df-lvols	⊢ LVols = ( 𝑘 ∈ V ↦ { 𝑥 ∈ ( Base ‘ 𝑘 ) ∣ ∃ 𝑝 ∈ ( LPlanes ‘ 𝑘 ) 𝑝 ( ⋖ ‘ 𝑘 ) 𝑥 } )

Detailed syntax breakdown

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