Definition df-pclN 30370

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 30417.) (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 30369	. 2 class PCl
2		vk	. . 3 set k
3		cvv 2916	. . 3 class _V
4		vx	. . . 4 set x
5	2	cv 1648	. . . . . 6 class k
6		catm 29746	. . . . . 6 class Atoms
7	5, 6	cfv 5413	. . . . 5 class ( Atoms ` k )
8	7	cpw 3759	. . . 4 class ~P ( Atoms ` k )
9	4	cv 1648	. . . . . . 7 class x
10		vy	. . . . . . . 8 set y
11	10	cv 1648	. . . . . . 7 class y
12	9, 11	wss 3280	. . . . . 6 wff x C_ y
13		cpsubsp 29978	. . . . . . 7 class PSubSp
14	5, 13	cfv 5413	. . . . . 6 class ( PSubSp ` k )
15	12, 10, 14	crab 2670	. . . . 5 class { y e. ( PSubSp ` k ) | x C_ y }
16	15	cint 4010	. . . 4 class |^| { y e. ( PSubSp ` k ) | x C_ y }
17	4, 8, 16	cmpt 4226	. . 3 class ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } )
18	2, 3, 17	cmpt 4226	. 2 class ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )
19	1, 18	wceq 1649	1 wff PCl = ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )

This definition is referenced by:  pclfvalN  30371