Definition df-pclN 35174

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 35221.) (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 35173	. 2 class PCl
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vx	. . . 4 setvar x
5	2	cv 1482	. . . . . 6 class k
6		catm 34550	. . . . . 6 class Atoms
7	5, 6	cfv 5888	. . . . 5 class ( Atoms ` k )
8	7	cpw 4158	. . . 4 class ~P ( Atoms ` k )
9	4	cv 1482	. . . . . . 7 class x
10		vy	. . . . . . . 8 setvar y
11	10	cv 1482	. . . . . . 7 class y
12	9, 11	wss 3574	. . . . . 6 wff x C_ y
13		cpsubsp 34782	. . . . . . 7 class PSubSp
14	5, 13	cfv 5888	. . . . . 6 class ( PSubSp ` k )
15	12, 10, 14	crab 2916	. . . . 5 class { y e. ( PSubSp ` k ) | x C_ y }
16	15	cint 4475	. . . 4 class |^| { y e. ( PSubSp ` k ) | x C_ y }
17	4, 8, 16	cmpt 4729	. . 3 class ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } )
18	2, 3, 17	cmpt 4729	. 2 class ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )
19	1, 18	wceq 1483	1 wff PCl = ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )

This definition is referenced by:  pclfvalN  35175