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