df-psubsp

Description: Define set of all projective subspaces. Based on definition of subspace in Holland95 p. 212. (Contributed by NM, 2-Oct-2011)

		Ref	Expression
	Assertion	df-psubsp	$⊢ PSubSp = (k \in V ⟼ \{s \| (s \subseteq Atoms (k) \land \forall p \in s \forall q \in s \forall r \in Atoms (k) (r \leq_{k} (p join (k) q) \to r \in s))\})$

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

Metamath Proof Explorer