Definition df-lines 35622

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 35615	. 2 class Lines
2		vk	. . 3 setvar k
3		cvv 3106	. . 3 class _V
4		vq	. . . . . . . . 9 setvar q
5	4	cv 1397	. . . . . . . 8 class q
6		vr	. . . . . . . . 9 setvar r
7	6	cv 1397	. . . . . . . 8 class r
8	5, 7	wne 2649	. . . . . . 7 wff q =/= r
9		vs	. . . . . . . . 9 setvar s
10	9	cv 1397	. . . . . . . 8 class s
11		vp	. . . . . . . . . . 11 setvar p
12	11	cv 1397	. . . . . . . . . 10 class p
13	2	cv 1397	. . . . . . . . . . . 12 class k
14		cjn 15772	. . . . . . . . . . . 12 class join
15	13, 14	cfv 5570	. . . . . . . . . . 11 class ( join ` k )
16	5, 7, 15	co 6270	. . . . . . . . . 10 class ( q ( join ` k ) r )
17		cple 14791	. . . . . . . . . . 11 class le
18	13, 17	cfv 5570	. . . . . . . . . 10 class ( le ` k )
19	12, 16, 18	wbr 4439	. . . . . . . . 9 wff p ( le ` k ) ( q ( join ` k ) r )
20		catm 35385	. . . . . . . . . 10 class Atoms
21	13, 20	cfv 5570	. . . . . . . . 9 class ( Atoms ` k )
22	19, 11, 21	crab 2808	. . . . . . . 8 class { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) }
23	10, 22	wceq 1398	. . . . . . 7 wff s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) }
24	8, 23	wa 367	. . . . . 6 wff ( q =/= r /\ s = { p e. ( Atoms ` k ) | p ( le ` k ) ( q ( join ` k ) r ) } )
25	24, 6, 21	wrex 2805	. . . . 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 2805	. . . 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 2439	. . 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 4497	. 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 1398	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  35859