Definition df-lvols 37521

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

Assertion

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

Distinct variable group:   𝑘,𝑝,𝑥

Detailed syntax breakdown of Definition df-lvols

Step	Hyp	Ref	Expression
1		clvol 37514	. 2 class LVols
2		vk	. . 3 setvar 𝑘
3		cvv 3433	. . 3 class V
4		vp	. . . . . . 7 setvar 𝑝
5	4	cv 1538	. . . . . 6 class 𝑝
6		vx	. . . . . . 7 setvar 𝑥
7	6	cv 1538	. . . . . 6 class 𝑥
8	2	cv 1538	. . . . . . 7 class 𝑘
9		ccvr 37283	. . . . . . 7 class ⋖
10	8, 9	cfv 6437	. . . . . 6 class ( ⋖ ‘𝑘)
11	5, 7, 10	wbr 5075	. . . . 5 wff 𝑝( ⋖ ‘𝑘)𝑥
12		clpl 37513	. . . . . 6 class LPlanes
13	8, 12	cfv 6437	. . . . 5 class (LPlanes‘𝑘)
14	11, 4, 13	wrex 3066	. . . 4 wff ∃𝑝 ∈ (LPlanes‘𝑘)𝑝( ⋖ ‘𝑘)𝑥
15		cbs 16921	. . . . 5 class Base
16	8, 15	cfv 6437	. . . 4 class (Base‘𝑘)
17	14, 6, 16	crab 3069	. . 3 class {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (LPlanes‘𝑘)𝑝( ⋖ ‘𝑘)𝑥}
18	2, 3, 17	cmpt 5158	. 2 class (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (LPlanes‘𝑘)𝑝( ⋖ ‘𝑘)𝑥})
19	1, 18	wceq 1539	1 wff LVols = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ ∃𝑝 ∈ (LPlanes‘𝑘)𝑝( ⋖ ‘𝑘)𝑥})

This definition is referenced by:  lvolset  37593