Metamath Proof Explorer

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 = k ∈ V ⟼ x ∈ Base k | ∃ p ∈ LPlanes ⁡ k p ⋖ k x

Detailed syntax breakdown

Step Hyp Ref Expression
0 clvol class LVols
1 vk setvar k
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar k
6 5 4 cfv class Base k
7 vp setvar p
8 clpl class LPlanes
9 5 8 cfv class LPlanes ⁡ k
10 7 cv setvar p
11 ccvr class ⋖
12 5 11 cfv class ⋖ k
13 3 cv setvar x
14 10 13 12 wbr wff p ⋖ k x
15 14 7 9 wrex wff ∃ p ∈ LPlanes ⁡ k p ⋖ k x
16 15 3 6 crab class x ∈ Base k | ∃ p ∈ LPlanes ⁡ k p ⋖ k x
17 1 2 16 cmpt class k ∈ V ⟼ x ∈ Base k | ∃ p ∈ LPlanes ⁡ k p ⋖ k x
18 0 17 wceq wff LVols = k ∈ V ⟼ x ∈ Base k | ∃ p ∈ LPlanes ⁡ k p ⋖ k x