Metamath Proof Explorer

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 clpl class LPlanes
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 clln class LLines
9 5 8 cfv class LLines ⁡ 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 ∈ LLines ⁡ k p ⋖ k x
16 15 3 6 crab class x ∈ Base k | ∃ p ∈ LLines ⁡ k p ⋖ k x
17 1 2 16 cmpt class k ∈ V ⟼ x ∈ Base k | ∃ p ∈ LLines ⁡ k p ⋖ k x
18 0 17 wceq wff LPlanes = k ∈ V ⟼ x ∈ Base k | ∃ p ∈ LLines ⁡ k p ⋖ k x