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 = (k \in V ⟼ \{s \| \exists q \in Atoms (k) \exists r \in Atoms (k) (q \neq r \land s = \{p \in Atoms (k) \| p \leq_{k} (q join (k) r)\})\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		clines	$class Lines$
1		vk	$setvar k$
2		cvv	$class V$
3		vs	$setvar s$
4		vq	$setvar q$
5		catm	$class Atoms$
6	1	cv	$setvar k$
7	6 5	cfv	$class Atoms (k)$
8		vr	$setvar r$
9	4	cv	$setvar q$
10	8	cv	$setvar r$
11	9 10	wne	$wff q \neq r$
12	3	cv	$setvar s$
13		vp	$setvar p$
14	13	cv	$setvar p$
15		cple	$class le$
16	6 15	cfv	$class \leq_{k}$
17		cjn	$class join$
18	6 17	cfv	$class join (k)$
19	9 10 18	co	$class (q join (k) r)$
20	14 19 16	wbr	$wff p \leq_{k} (q join (k) r)$
21	20 13 7	crab	$class \{p \in Atoms (k) \| p \leq_{k} (q join (k) r)\}$
22	12 21	wceq	$wff s = \{p \in Atoms (k) \| p \leq_{k} (q join (k) r)\}$
23	11 22	wa	$wff (q \neq r \land s = \{p \in Atoms (k) \| p \leq_{k} (q join (k) r)\})$
24	23 8 7	wrex	$wff \exists r \in Atoms (k) (q \neq r \land s = \{p \in Atoms (k) \| p \leq_{k} (q join (k) r)\})$
25	24 4 7	wrex	$wff \exists q \in Atoms (k) \exists r \in Atoms (k) (q \neq r \land s = \{p \in Atoms (k) \| p \leq_{k} (q join (k) r)\})$
26	25 3	cab	$class \{s \| \exists q \in Atoms (k) \exists r \in Atoms (k) (q \neq r \land s = \{p \in Atoms (k) \| p \leq_{k} (q join (k) r)\})\}$
27	1 2 26	cmpt	$class (k \in V ⟼ \{s \| \exists q \in Atoms (k) \exists r \in Atoms (k) (q \neq r \land s = \{p \in Atoms (k) \| p \leq_{k} (q join (k) r)\})\})$
28	0 27	wceq	$wff Lines = (k \in V ⟼ \{s \| \exists q \in Atoms (k) \exists r \in Atoms (k) (q \neq r \land s = \{p \in Atoms (k) \| p \leq_{k} (q join (k) r)\})\})$

Metamath Proof Explorer

Definition df-lines

Detailed syntax breakdown