Definition df-pclN 38754

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 38801.) (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 38753	. 2 class PCl
2		vk	. . 3 setvar 𝑘
3		cvv 3474	. . 3 class V
4		vx	. . . 4 setvar 𝑥
5	2	cv 1540	. . . . . 6 class 𝑘
6		catm 38128	. . . . . 6 class Atoms
7	5, 6	cfv 6543	. . . . 5 class (Atoms‘𝑘)
8	7	cpw 4602	. . . 4 class 𝒫 (Atoms‘𝑘)
9	4	cv 1540	. . . . . . 7 class 𝑥
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1540	. . . . . . 7 class 𝑦
12	9, 11	wss 3948	. . . . . 6 wff 𝑥 ⊆ 𝑦
13		cpsubsp 38362	. . . . . . 7 class PSubSp
14	5, 13	cfv 6543	. . . . . 6 class (PSubSp‘𝑘)
15	12, 10, 14	crab 3432	. . . . 5 class {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}
16	15	cint 4950	. . . 4 class ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}
17	4, 8, 16	cmpt 5231	. . 3 class (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦})
18	2, 3, 17	cmpt 5231	. 2 class (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}))
19	1, 18	wceq 1541	1 wff PCl = (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}))

This definition is referenced by:  pclfvalN  38755