Metamath Proof Explorer


Definition df-llines

Description: Define the set of all "lattice lines" (lattice elements which cover an atom) in a Hilbert lattice k , in other words all elements of height 2 (or lattice dimension 2 or projective dimension 1). (Contributed by NM, 16-Jun-2012)

Ref Expression
Assertion df-llines LLines = k V x Base k | p Atoms k p k x

Detailed syntax breakdown

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