Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-lines Structured version   Unicode version

Definition df-lines 33150
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.)
Assertion
Ref Expression
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 ) } ) } )
Distinct variable group:    k, p, q, r, s

Detailed syntax breakdown of Definition df-lines
StepHypRef Expression
1 clines 33143 . 2  class  Lines
2 vk . . 3  setvar  k
3 cvv 2977 . . 3  class  _V
4 vq . . . . . . . . 9  setvar  q
54cv 1368 . . . . . . . 8  class  q
6 vr . . . . . . . . 9  setvar  r
76cv 1368 . . . . . . . 8  class  r
85, 7wne 2611 . . . . . . 7  wff  q  =/=  r
9 vs . . . . . . . . 9  setvar  s
109cv 1368 . . . . . . . 8  class  s
11 vp . . . . . . . . . . 11  setvar  p
1211cv 1368 . . . . . . . . . 10  class  p
132cv 1368 . . . . . . . . . . . 12  class  k
14 cjn 15119 . . . . . . . . . . . 12  class  join
1513, 14cfv 5423 . . . . . . . . . . 11  class  ( join `  k )
165, 7, 15co 6096 . . . . . . . . . 10  class  ( q ( join `  k
) r )
17 cple 14250 . . . . . . . . . . 11  class  le
1813, 17cfv 5423 . . . . . . . . . 10  class  ( le
`  k )
1912, 16, 18wbr 4297 . . . . . . . . 9  wff  p ( le `  k ) ( q ( join `  k ) r )
20 catm 32913 . . . . . . . . . 10  class  Atoms
2113, 20cfv 5423 . . . . . . . . 9  class  ( Atoms `  k )
2219, 11, 21crab 2724 . . . . . . . 8  class  { p  e.  ( Atoms `  k )  |  p ( le `  k ) ( q ( join `  k
) r ) }
2310, 22wceq 1369 . . . . . . 7  wff  s  =  { p  e.  (
Atoms `  k )  |  p ( le `  k ) ( q ( join `  k
) r ) }
248, 23wa 369 . . . . . 6  wff  ( q  =/=  r  /\  s  =  { p  e.  (
Atoms `  k )  |  p ( le `  k ) ( q ( join `  k
) r ) } )
2524, 6, 21wrex 2721 . . . . 5  wff  E. r  e.  ( Atoms `  k )
( q  =/=  r  /\  s  =  {
p  e.  ( Atoms `  k )  |  p ( le `  k
) ( q (
join `  k )
r ) } )
2625, 4, 21wrex 2721 . . . 4  wff  E. q  e.  ( Atoms `  k ) E. r  e.  ( Atoms `  k ) ( q  =/=  r  /\  s  =  { p  e.  ( Atoms `  k )  |  p ( le `  k ) ( q ( join `  k
) r ) } )
2726, 9cab 2429 . . 3  class  { 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 ) } ) }
282, 3, 27cmpt 4355 . 2  class  ( 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 ) } ) } )
291, 28wceq 1369 1  wff  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 ) } ) } )
Colors of variables: wff setvar class
This definition is referenced by:  lineset  33387
  Copyright terms: Public domain W3C validator