Definition df-psubclN 41183

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 41182	. 2 class PSubCl
2		vk	. . 3 setvar 𝑘
3		cvv 3454	. . 3 class V
4		vs	. . . . . . 7 setvar 𝑠
5	4	cv 1569	. . . . . 6 class 𝑠
6	2	cv 1569	. . . . . . 7 class 𝑘
7		catm 40511	. . . . . . 7 class Atoms
8	6, 7	cfv 6555	. . . . . 6 class (Atoms‘𝑘)
9	5, 8	wss 3900	. . . . 5 wff 𝑠 ⊆ (Atoms‘𝑘)
10		cpolN 41150	. . . . . . . . 9 class ⊥𝑃
11	6, 10	cfv 6555	. . . . . . . 8 class (⊥𝑃‘𝑘)
12	5, 11	cfv 6555	. . . . . . 7 class ((⊥𝑃‘𝑘)‘𝑠)
13	12, 11	cfv 6555	. . . . . 6 class ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠))
14	13, 5	wceq 1570	. . . . 5 wff ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠
15	9, 14	wa 401	. . . 4 wff (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)
16	15, 4	cab 2741	. . 3 class {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)}
17	2, 3, 16	cmpt 5189	. 2 class (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)})
18	1, 17	wceq 1570	1 wff PSubCl = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)})

This definition is used by:  psubclsetN  41184