Definition df-lines 29983

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

Step	Hyp	Ref	Expression
1		clines 29976	. 2 class Lines
2		vk	. . 3 set k
3		cvv 2916	. . 3 class _V
4		vq	. . . . . . . . 9 set q
5	4	cv 1648	. . . . . . . 8 class q
6		vr	. . . . . . . . 9 set r
7	6	cv 1648	. . . . . . . 8 class r
8	5, 7	wne 2567	. . . . . . 7 wff q =/= r
9		vs	. . . . . . . . 9 set s
10	9	cv 1648	. . . . . . . 8 class s
11		vp	. . . . . . . . . . 11 set p
12	11	cv 1648	. . . . . . . . . 10 class p
13	2	cv 1648	. . . . . . . . . . . 12 class k
14		cjn 14356	. . . . . . . . . . . 12 class join
15	13, 14	cfv 5413	. . . . . . . . . . 11 class ( join ` k )
16	5, 7, 15	co 6040	. . . . . . . . . 10 class ( q ( join ` k ) r )
17		cple 13491	. . . . . . . . . . 11 class le
18	13, 17	cfv 5413	. . . . . . . . . 10 class ( le ` k )
19	12, 16, 18	wbr 4172	. . . . . . . . 9 wff p ( le ` k ) ( q ( join ` k ) r )
20		catm 29746	. . . . . . . . . 10 class Atoms
21	13, 20	cfv 5413	. . . . . . . . 9 class ( Atoms ` k )
22	19, 11, 21	crab 2670	. . . . . . . 8 class { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) }
23	10, 22	wceq 1649	. . . . . . 7 wff s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) }
24	8, 23	wa 359	. . . . . 6 wff ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } )
25	24, 6, 21	wrex 2667	. . . . 5 wff E. r e. ( Atoms ` k ) ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } )
26	25, 4, 21	wrex 2667	. . . 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 ) } )
27	26, 9	cab 2390	. . 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 ) } ) }
28	2, 3, 27	cmpt 4226	. 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 ) } ) } )
29	1, 28	wceq 1649	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 ) } ) } )

This definition is referenced by:  lineset  30220