Definition df-lines 38310

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 38303	. 2 class Lines
2		vk	. . 3 setvar 𝑘
3		cvv 3475	. . 3 class V
4		vq	. . . . . . . . 9 setvar 𝑞
5	4	cv 1541	. . . . . . . 8 class 𝑞
6		vr	. . . . . . . . 9 setvar 𝑟
7	6	cv 1541	. . . . . . . 8 class 𝑟
8	5, 7	wne 2941	. . . . . . 7 wff 𝑞 ≠ 𝑟
9		vs	. . . . . . . . 9 setvar 𝑠
10	9	cv 1541	. . . . . . . 8 class 𝑠
11		vp	. . . . . . . . . . 11 setvar 𝑝
12	11	cv 1541	. . . . . . . . . 10 class 𝑝
13	2	cv 1541	. . . . . . . . . . . 12 class 𝑘
14		cjn 18260	. . . . . . . . . . . 12 class join
15	13, 14	cfv 6540	. . . . . . . . . . 11 class (join‘𝑘)
16	5, 7, 15	co 7404	. . . . . . . . . 10 class (𝑞(join‘𝑘)𝑟)
17		cple 17200	. . . . . . . . . . 11 class le
18	13, 17	cfv 6540	. . . . . . . . . 10 class (le‘𝑘)
19	12, 16, 18	wbr 5147	. . . . . . . . 9 wff 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)
20		catm 38071	. . . . . . . . . 10 class Atoms
21	13, 20	cfv 6540	. . . . . . . . 9 class (Atoms‘𝑘)
22	19, 11, 21	crab 3433	. . . . . . . 8 class {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}
23	10, 22	wceq 1542	. . . . . . 7 wff 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}
24	8, 23	wa 397	. . . . . 6 wff (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})
25	24, 6, 21	wrex 3071	. . . . 5 wff ∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})
26	25, 4, 21	wrex 3071	. . . 4 wff ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})
27	26, 9	cab 2710	. . 3 class {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})}
28	2, 3, 27	cmpt 5230	. 2 class (𝑘 ∈ V ↦ {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})})
29	1, 28	wceq 1542	1 wff Lines = (𝑘 ∈ V ↦ {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})})

This definition is referenced by:  lineset  38547