Definition df-lines 33805

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 33798	. 2 class Lines
2		vk	. . 3 setvar 𝑘
3		cvv 3173	. . 3 class V
4		vq	. . . . . . . . 9 setvar 𝑞
5	4	cv 1474	. . . . . . . 8 class 𝑞
6		vr	. . . . . . . . 9 setvar 𝑟
7	6	cv 1474	. . . . . . . 8 class 𝑟
8	5, 7	wne 2780	. . . . . . 7 wff 𝑞 ≠ 𝑟
9		vs	. . . . . . . . 9 setvar 𝑠
10	9	cv 1474	. . . . . . . 8 class 𝑠
11		vp	. . . . . . . . . . 11 setvar 𝑝
12	11	cv 1474	. . . . . . . . . 10 class 𝑝
13	2	cv 1474	. . . . . . . . . . . 12 class 𝑘
14		cjn 16767	. . . . . . . . . . . 12 class join
15	13, 14	cfv 5804	. . . . . . . . . . 11 class (join‘𝑘)
16	5, 7, 15	co 6549	. . . . . . . . . 10 class (𝑞(join‘𝑘)𝑟)
17		cple 15775	. . . . . . . . . . 11 class le
18	13, 17	cfv 5804	. . . . . . . . . 10 class (le‘𝑘)
19	12, 16, 18	wbr 4583	. . . . . . . . 9 wff 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)
20		catm 33568	. . . . . . . . . 10 class Atoms
21	13, 20	cfv 5804	. . . . . . . . 9 class (Atoms‘𝑘)
22	19, 11, 21	crab 2900	. . . . . . . 8 class {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}
23	10, 22	wceq 1475	. . . . . . 7 wff 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)}
24	8, 23	wa 383	. . . . . 6 wff (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})
25	24, 6, 21	wrex 2897	. . . . 5 wff ∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})
26	25, 4, 21	wrex 2897	. . . 4 wff ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})
27	26, 9	cab 2596	. . 3 class {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})}
28	2, 3, 27	cmpt 4643	. 2 class (𝑘 ∈ V ↦ {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})})
29	1, 28	wceq 1475	1 wff Lines = (𝑘 ∈ V ↦ {𝑠 ∣ ∃𝑞 ∈ (Atoms‘𝑘)∃𝑟 ∈ (Atoms‘𝑘)(𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ (Atoms‘𝑘) ∣ 𝑝(le‘𝑘)(𝑞(join‘𝑘)𝑟)})})

This definition is referenced by:  lineset  34042