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 e. _V |-> { s | E. q e. ( Atoms ` k ) E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 clines 
 |-  Lines
1 vk 
 |-  k
2 cvv 
 |-  _V
3 vs 
 |-  s
4 vq 
 |-  q
5 catm 
 |-  Atoms
6 1 cv 
 |-  k
7 6 5 cfv 
 |-  ( Atoms ` k )
8 vr 
 |-  r
9 4 cv 
 |-  q
10 8 cv 
 |-  r
11 9 10 wne 
 |-  q =/= r
12 3 cv 
 |-  s
13 vp 
 |-  p
14 13 cv 
 |-  p
15 cple 
 |-  le
16 6 15 cfv 
 |-  ( le ` k )
17 cjn 
 |-  join
18 6 17 cfv 
 |-  ( join ` k )
19 9 10 18 co 
 |-  ( q ( join ` k ) r )
20 14 19 16 wbr 
 |-  p ( le ` k ) ( q ( join ` k ) r )
21 20 13 7 crab 
 |-  { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) }
22 12 21 wceq 
 |-  s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) }
23 11 22 wa 
 |-  ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } )
24 23 8 7 wrex 
 |-  E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } )
25 24 4 7 wrex 
 |-  E. q e. ( Atoms ` k ) E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } )
26 25 3 cab 
 |-  { s | E. q e. ( Atoms ` k ) E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } ) }
27 1 2 26 cmpt 
 |-  ( k e. _V |-> { s | E. q e. ( Atoms ` k ) E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } ) } )
28 0 27 wceq 
 |-  Lines = ( k e. _V |-> { s | E. q e. ( Atoms ` k ) E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } ) } )