Metamath Proof Explorer

Definition df-pclN

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 .) (Contributed by NM, 7-Sep-2013)

Ref Expression
Assertion df-pclN ⊢ PCl = k ∈ V ⟼ x ∈ 𝒫 Atoms ⁡ k ⟼ ⋂ y ∈ PSubSp ⁡ k | x ⊆ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cpclN class PCl
1 vk setvar k
2 cvv class V
3 vx setvar x
4 catm class Atoms
5 1 cv setvar k
6 5 4 cfv class Atoms ⁡ k
7 6 cpw class 𝒫 Atoms ⁡ k
8 vy setvar y
9 cpsubsp class PSubSp
10 5 9 cfv class PSubSp ⁡ k
11 3 cv setvar x
12 8 cv setvar y
13 11 12 wss wff x ⊆ y
14 13 8 10 crab class y ∈ PSubSp ⁡ k | x ⊆ y
15 14 cint class ⋂ y ∈ PSubSp ⁡ k | x ⊆ y
16 3 7 15 cmpt class x ∈ 𝒫 Atoms ⁡ k ⟼ ⋂ y ∈ PSubSp ⁡ k | x ⊆ y
17 1 2 16 cmpt class k ∈ V ⟼ x ∈ 𝒫 Atoms ⁡ k ⟼ ⋂ y ∈ PSubSp ⁡ k | x ⊆ y
18 0 17 wceq wff PCl = k ∈ V ⟼ x ∈ 𝒫 Atoms ⁡ k ⟼ ⋂ y ∈ PSubSp ⁡ k | x ⊆ y