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 = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clines	⊢ Lines
1		vk	⊢ 𝑘
2		cvv	⊢ V
3		vs	⊢ 𝑠
4		vq	⊢ 𝑞
5		catm	⊢ Atoms
6	1	cv	⊢ 𝑘
7	6 5	cfv	⊢ ( Atoms ‘ 𝑘 )
8		vr	⊢ 𝑟
9	4	cv	⊢ 𝑞
10	8	cv	⊢ 𝑟
11	9 10	wne	⊢ 𝑞 ≠ 𝑟
12	3	cv	⊢ 𝑠
13		vp	⊢ 𝑝
14	13	cv	⊢ 𝑝
15		cple	⊢ le
16	6 15	cfv	⊢ ( le ‘ 𝑘 )
17		cjn	⊢ join
18	6 17	cfv	⊢ ( join ‘ 𝑘 )
19	9 10 18	co	⊢ ( 𝑞 ( join ‘ 𝑘 ) 𝑟 )
20	14 19 16	wbr	⊢ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 )
21	20 13 7	crab	⊢ { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) }
22	12 21	wceq	⊢ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) }
23	11 22	wa	⊢ ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } )
24	23 8 7	wrex	⊢ ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } )
25	24 4 7	wrex	⊢ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } )
26	25 3	cab	⊢ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) }
27	1 2 26	cmpt	⊢ ( 𝑘 ∈ V ↦ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } )
28	0 27	wceq	⊢ Lines = ( 𝑘 ∈ V ↦ { 𝑠 ∣ ∃ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ∃ 𝑟 ∈ ( Atoms ‘ 𝑘 ) ( 𝑞 ≠ 𝑟 ∧ 𝑠 = { 𝑝 ∈ ( Atoms ‘ 𝑘 ) ∣ 𝑝 ( le ‘ 𝑘 ) ( 𝑞 ( join ‘ 𝑘 ) 𝑟 ) } ) } )