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 35742
 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 35741 . 2 class PSubCl
2 vk . . 3 setvar 𝑘
3 cvv 3340 . . 3 class V
4 vs . . . . . . 7 setvar 𝑠
54cv 1631 . . . . . 6 class 𝑠
62cv 1631 . . . . . . 7 class 𝑘
7 catm 35071 . . . . . . 7 class Atoms
86, 7cfv 6049 . . . . . 6 class (Atoms‘𝑘)
95, 8wss 3715 . . . . 5 wff 𝑠 ⊆ (Atoms‘𝑘)
10 cpolN 35709 . . . . . . . . 9 class 𝑃
116, 10cfv 6049 . . . . . . . 8 class (⊥𝑃𝑘)
125, 11cfv 6049 . . . . . . 7 class ((⊥𝑃𝑘)‘𝑠)
1312, 11cfv 6049 . . . . . 6 class ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠))
1413, 5wceq 1632 . . . . 5 wff ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠
159, 14wa 383 . . . 4 wff (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠)
1615, 4cab 2746 . . 3 class {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠)}
172, 3, 16cmpt 4881 . 2 class (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠)})
181, 17wceq 1632 1 wff PSubCl = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃𝑘)‘((⊥𝑃𝑘)‘𝑠)) = 𝑠)})
 Colors of variables: wff setvar class This definition is referenced by:  psubclsetN  35743
 Copyright terms: Public domain W3C validator