Metamath Proof Explorer

Definition df-psubclN

Description: Define set of all closed projective subspaces, which are those sets of atoms that equal their double polarity. Based on definition in Holland95 p. 223. (Contributed by NM, 23-Jan-2012)

		Ref	Expression
	Assertion	df-psubclN	$⊢ PSubCl = (k \in V ⟼ \{s \| (s \subseteq Atoms (k) \land ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s)\})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpscN	$class PSubCl$
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		cpolN	$class ⊥_{𝑃}$
10	6 9	cfv	$class ⊥_{𝑃} (k)$
11	4 10	cfv	$class ⊥_{𝑃} (k) (s)$
12	11 10	cfv	$class ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s))$
13	12 4	wceq	$wff ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s$
14	8 13	wa	$wff (s \subseteq Atoms (k) \land ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s)$
15	14 3	cab	$class \{s \| (s \subseteq Atoms (k) \land ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s)\}$
16	1 2 15	cmpt	$class (k \in V ⟼ \{s \| (s \subseteq Atoms (k) \land ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s)\})$
17	0 16	wceq	$wff PSubCl = (k \in V ⟼ \{s \| (s \subseteq Atoms (k) \land ⊥_{𝑃} (k) (⊥_{𝑃} (k) (s)) = s)\})$