Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-psubclN Structured version   Visualization version   GIF version

Definition df-psubclN 34038
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
StepHypRef Expression
1 cpscN 34037 . 2 class PSubCl
2 vk . . 3 setvar 𝑘
3 cvv 3168 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1473 . . . . . 6 class 𝑠
62cv 1473 . . . . . . 7 class 𝑘
7 catm 33367 . . . . . . 7 class Atoms
86, 7cfv 5786 . . . . . 6 class (Atoms‘𝑘)
95, 8wss 3535 . . . . 5 wff 𝑠 ⊆ (Atoms‘𝑘)
10 cpolN 34005 . . . . . . . . 9 class 𝑃
116, 10cfv 5786 . . . . . . . 8 class (⊥𝑃𝑘)
125, 11cfv 5786 . . . . . . 7 class ((⊥𝑃𝑘)‘𝑠)
1312, 11cfv 5786 . . . . . 6 class ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠))
1413, 5wceq 1474 . . . . 5 wff ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠
159, 14wa 382 . . . 4 wff (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠)
1615, 4cab 2591 . . 3 class {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠)}
172, 3, 16cmpt 4633 . 2 class (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠)})
181, 17wceq 1474 1 wff PSubCl = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠)})
Colors of variables: wff setvar class
This definition is referenced by:  psubclsetN  34039
  Copyright terms: Public domain W3C validator