Metamath Proof Explorer

Definition df-lines

Description: Define set of all projective lines for a Hilbert lattice (actually in any set at all, for simplicity). The join of two distinct atoms equals a line. Definition of lines in item 1 of Holland95 p. 222. (Contributed by NM, 19-Sep-2011)

Ref Expression
Assertion df-lines ⊢ Lines = k ∈ V ⟼ s | ∃ q ∈ Atoms ⁡ k ∃ r ∈ Atoms ⁡ k q ≠ r ∧ s = p ∈ Atoms ⁡ k | p ≤ k q join ⁡ k r

Detailed syntax breakdown

Step Hyp Ref Expression
0 clines class Lines
1 vk setvar k
2 cvv class V
3 vs setvar s
4 vq setvar q
5 catm class Atoms
6 1 cv setvar k
7 6 5 cfv class Atoms ⁡ k
8 vr setvar r
9 4 cv setvar q
10 8 cv setvar r
11 9 10 wne wff q ≠ r
12 3 cv setvar s
13 vp setvar p
14 13 cv setvar p
15 cple class le
16 6 15 cfv class ≤ k
17 cjn class join
18 6 17 cfv class join ⁡ k
19 9 10 18 co class q join ⁡ k r
20 14 19 16 wbr wff p ≤ k q join ⁡ k r
21 20 13 7 crab class p ∈ Atoms ⁡ k | p ≤ k q join ⁡ k r
22 12 21 wceq wff s = p ∈ Atoms ⁡ k | p ≤ k q join ⁡ k r
23 11 22 wa wff q ≠ r ∧ s = p ∈ Atoms ⁡ k | p ≤ k q join ⁡ k r
24 23 8 7 wrex wff ∃ r ∈ Atoms ⁡ k q ≠ r ∧ s = p ∈ Atoms ⁡ k | p ≤ k q join ⁡ k r
25 24 4 7 wrex wff ∃ q ∈ Atoms ⁡ k ∃ r ∈ Atoms ⁡ k q ≠ r ∧ s = p ∈ Atoms ⁡ k | p ≤ k q join ⁡ k r
26 25 3 cab class s | ∃ q ∈ Atoms ⁡ k ∃ r ∈ Atoms ⁡ k q ≠ r ∧ s = p ∈ Atoms ⁡ k | p ≤ k q join ⁡ k r
27 1 2 26 cmpt class k ∈ V ⟼ s | ∃ q ∈ Atoms ⁡ k ∃ r ∈ Atoms ⁡ k q ≠ r ∧ s = p ∈ Atoms ⁡ k | p ≤ k q join ⁡ k r
28 0 27 wceq wff Lines = k ∈ V ⟼ s | ∃ q ∈ Atoms ⁡ k ∃ r ∈ Atoms ⁡ k q ≠ r ∧ s = p ∈ Atoms ⁡ k | p ≤ k q join ⁡ k r