Definition df-psubclN 34239

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.)

Assertion

Ref	Expression
df-psubclN	⊢ PSubCl = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)})

Distinct variable group:   𝑘,𝑠

Detailed syntax breakdown of Definition df-psubclN

Step	Hyp	Ref	Expression
1		cpscN 34238	. 2 class PSubCl
2		vk	. . 3 setvar 𝑘
3		cvv 3173	. . 3 class V
4		vs	. . . . . . 7 setvar 𝑠
5	4	cv 1474	. . . . . 6 class 𝑠
6	2	cv 1474	. . . . . . 7 class 𝑘
7		catm 33568	. . . . . . 7 class Atoms
8	6, 7	cfv 5804	. . . . . 6 class (Atoms‘𝑘)
9	5, 8	wss 3540	. . . . 5 wff 𝑠 ⊆ (Atoms‘𝑘)
10		cpolN 34206	. . . . . . . . 9 class ⊥𝑃
11	6, 10	cfv 5804	. . . . . . . 8 class (⊥𝑃‘𝑘)
12	5, 11	cfv 5804	. . . . . . 7 class ((⊥𝑃‘𝑘)‘𝑠)
13	12, 11	cfv 5804	. . . . . 6 class ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠))
14	13, 5	wceq 1475	. . . . 5 wff ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠
15	9, 14	wa 383	. . . 4 wff (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)
16	15, 4	cab 2596	. . 3 class {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)}
17	2, 3, 16	cmpt 4643	. 2 class (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)})
18	1, 17	wceq 1475	1 wff PSubCl = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)})

This definition is referenced by:  psubclsetN  34240