Definition df-lines 33036

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 33029	. 2 class Lines
2		vk	. . 3 setvar k
3		cvv 3080	. . 3 class _V
4		vq	. . . . . . . . 9 setvar q
5	4	cv 1436	. . . . . . . 8 class q
6		vr	. . . . . . . . 9 setvar r
7	6	cv 1436	. . . . . . . 8 class r
8	5, 7	wne 2614	. . . . . . 7 wff q =/= r
9		vs	. . . . . . . . 9 setvar s
10	9	cv 1436	. . . . . . . 8 class s
11		vp	. . . . . . . . . . 11 setvar p
12	11	cv 1436	. . . . . . . . . 10 class p
13	2	cv 1436	. . . . . . . . . . . 12 class k
14		cjn 16189	. . . . . . . . . . . 12 class join
15	13, 14	cfv 5601	. . . . . . . . . . 11 class ( join ` k )
16	5, 7, 15	co 6306	. . . . . . . . . 10 class ( q ( join ` k ) r )
17		cple 15197	. . . . . . . . . . 11 class le
18	13, 17	cfv 5601	. . . . . . . . . 10 class ( le ` k )
19	12, 16, 18	wbr 4423	. . . . . . . . 9 wff p ( le ` k ) ( q ( join ` k ) r )
20		catm 32799	. . . . . . . . . 10 class Atoms
21	13, 20	cfv 5601	. . . . . . . . 9 class ( Atoms ` k )
22	19, 11, 21	crab 2775	. . . . . . . 8 class { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) }
23	10, 22	wceq 1437	. . . . . . 7 wff s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) }
24	8, 23	wa 370	. . . . . 6 wff ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } )
25	24, 6, 21	wrex 2772	. . . . 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 2772	. . . 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 2407	. . 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 4482	. 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 1437	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  33273