Definition df-lines 39503

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

Distinct variable group:   𝑘,𝑝,𝑞,𝑟,𝑠

Detailed syntax breakdown of Definition df-lines

Step	Hyp	Ref	Expression
1		clines 39496	. 2 class Lines
2		vk	. . 3 setvar 𝑘
3		cvv 3480	. . 3 class V
4		vq	. . . . . . . . 9 setvar 𝑞
5	4	cv 1539	. . . . . . . 8 class 𝑞
6		vr	. . . . . . . . 9 setvar 𝑟
7	6	cv 1539	. . . . . . . 8 class 𝑟
8	5, 7	wne 2940	. . . . . . 7 wff 𝑞 ≠ 𝑟
9		vs	. . . . . . . . 9 setvar 𝑠
10	9	cv 1539	. . . . . . . 8 class 𝑠
11		vp	. . . . . . . . . . 11 setvar 𝑝
12	11	cv 1539	. . . . . . . . . 10 class 𝑝
13	2	cv 1539	. . . . . . . . . . . 12 class 𝑘
14		cjn 18357	. . . . . . . . . . . 12 class join
15	13, 14	cfv 6561	. . . . . . . . . . 11 class (join‘𝑘)
16	5, 7, 15	co 7431	. . . . . . . . . 10 class (𝑞(join‘𝑘)𝑟)
17		cple 17304	. . . . . . . . . . 11 class le
18	13, 17	cfv 6561	. . . . . . . . . 10 class (le‘𝑘)
19	12, 16, 18	wbr 5143	. . . . . . . . 9 wff 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)
20		catm 39264	. . . . . . . . . 10 class Atoms
21	13, 20	cfv 6561	. . . . . . . . 9 class (Atoms‘𝑘)
22	19, 11, 21	crab 3436	. . . . . . . 8 class {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}
23	10, 22	wceq 1540	. . . . . . 7 wff 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}
24	8, 23	wa 395	. . . . . 6 wff (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})
25	24, 6, 21	wrex 3070	. . . . 5 wff ∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})
26	25, 4, 21	wrex 3070	. . . 4 wff ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})
27	26, 9	cab 2714	. . 3 class {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})}
28	2, 3, 27	cmpt 5225	. 2 class (𝑘 ∈ V ↦ {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})})
29	1, 28	wceq 1540	1 wff Lines = (𝑘 ∈ V ↦ {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})})

This definition is referenced by:  lineset  39740