Definition df-pclN 30622

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

Assertion

Ref	Expression
df-pclN	|- PCl = ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )

Distinct variable group:   x, k, y

Detailed syntax breakdown of Definition df-pclN

Step	Hyp	Ref	Expression
1		cpclN 30621	. 2 class PCl
2		vk	. . 3 set k
3		cvv 2948	. . 3 class _V
4		vx	. . . 4 set x
5	2	cv 1651	. . . . . 6 class k
6		catm 29998	. . . . . 6 class Atoms
7	5, 6	cfv 5446	. . . . 5 class ( Atoms ` k )
8	7	cpw 3791	. . . 4 class ~P ( Atoms ` k )
9	4	cv 1651	. . . . . . 7 class x
10		vy	. . . . . . . 8 set y
11	10	cv 1651	. . . . . . 7 class y
12	9, 11	wss 3312	. . . . . 6 wff x C_ y
13		cpsubsp 30230	. . . . . . 7 class PSubSp
14	5, 13	cfv 5446	. . . . . 6 class ( PSubSp ` k )
15	12, 10, 14	crab 2701	. . . . 5 class { y e. ( PSubSp ` k ) | x C_ y }
16	15	cint 4042	. . . 4 class |^| { y e. ( PSubSp ` k ) | x C_ y }
17	4, 8, 16	cmpt 4258	. . 3 class ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } )
18	2, 3, 17	cmpt 4258	. 2 class ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )
19	1, 18	wceq 1652	1 wff PCl = ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )

This definition is referenced by:  pclfvalN  30623