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

Definition df-pclN 38759
Description: Projective subspace closure, which is the smallest projective subspace containing an arbitrary set of atoms. The subspace closure of the union of a set of projective subspaces is their supremum in PSubSp. Related to an analogous definition of closure used in Lemma 3.1.4 of [PtakPulmannova] p. 68. (Note that this closure is not necessarily one of the closed projective subspaces PSubCl of df-psubclN 38806.) (Contributed by NM, 7-Sep-2013.)
Assertion
Ref Expression
df-pclN PCl = (π‘˜ ∈ V ↦ (π‘₯ ∈ 𝒫 (Atomsβ€˜π‘˜) ↦ ∩ {𝑦 ∈ (PSubSpβ€˜π‘˜) ∣ π‘₯ βŠ† 𝑦}))
Distinct variable group:   π‘₯,π‘˜,𝑦

Detailed syntax breakdown of Definition df-pclN
StepHypRef Expression
1 cpclN 38758 . 2 class PCl
2 vk . . 3 setvar π‘˜
3 cvv 3475 . . 3 class V
4 vx . . . 4 setvar π‘₯
52cv 1541 . . . . . 6 class π‘˜
6 catm 38133 . . . . . 6 class Atoms
75, 6cfv 6544 . . . . 5 class (Atomsβ€˜π‘˜)
87cpw 4603 . . . 4 class 𝒫 (Atomsβ€˜π‘˜)
94cv 1541 . . . . . . 7 class π‘₯
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1541 . . . . . . 7 class 𝑦
129, 11wss 3949 . . . . . 6 wff π‘₯ βŠ† 𝑦
13 cpsubsp 38367 . . . . . . 7 class PSubSp
145, 13cfv 6544 . . . . . 6 class (PSubSpβ€˜π‘˜)
1512, 10, 14crab 3433 . . . . 5 class {𝑦 ∈ (PSubSpβ€˜π‘˜) ∣ π‘₯ βŠ† 𝑦}
1615cint 4951 . . . 4 class ∩ {𝑦 ∈ (PSubSpβ€˜π‘˜) ∣ π‘₯ βŠ† 𝑦}
174, 8, 16cmpt 5232 . . 3 class (π‘₯ ∈ 𝒫 (Atomsβ€˜π‘˜) ↦ ∩ {𝑦 ∈ (PSubSpβ€˜π‘˜) ∣ π‘₯ βŠ† 𝑦})
182, 3, 17cmpt 5232 . 2 class (π‘˜ ∈ V ↦ (π‘₯ ∈ 𝒫 (Atomsβ€˜π‘˜) ↦ ∩ {𝑦 ∈ (PSubSpβ€˜π‘˜) ∣ π‘₯ βŠ† 𝑦}))
191, 18wceq 1542 1 wff PCl = (π‘˜ ∈ V ↦ (π‘₯ ∈ 𝒫 (Atomsβ€˜π‘˜) ↦ ∩ {𝑦 ∈ (PSubSpβ€˜π‘˜) ∣ π‘₯ βŠ† 𝑦}))
Colors of variables: wff setvar class
This definition is referenced by:  pclfvalN  38760
  Copyright terms: Public domain W3C validator