Definition df-pclN 38807

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

Step	Hyp	Ref	Expression
1		cpclN 38806	. 2 class PCl
2		vk	. . 3 setvar 𝑘
3		cvv 3475	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1541	. . . . . 6 class 𝑘
6		catm 38181	. . . . . 6 class Atoms
7	5, 6	cfv 6544	. . . . 5 class (Atoms‘𝑘)
8	7	cpw 4603	. . . 4 class 𝒫 (Atoms‘𝑘)
9	4	cv 1541	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1541	. . . . . . 7 class 𝑦
12	9, 11	wss 3949	. . . . . 6 wff 𝑥 ⊆ 𝑦
13		cpsubsp 38415	. . . . . . 7 class PSubSp
14	5, 13	cfv 6544	. . . . . 6 class (PSubSp‘𝑘)
15	12, 10, 14	crab 3433	. . . . 5 class {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}
16	15	cint 4951	. . . 4 class ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}
17	4, 8, 16	cmpt 5232	. . 3 class (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦})
18	2, 3, 17	cmpt 5232	. 2 class (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}))
19	1, 18	wceq 1542	1 wff PCl = (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}))

This definition is referenced by:  pclfvalN  38808