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 e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpclN	|- PCl
1		vk	|- k
2		cvv	|- _V
3		vx	|- x
4		catm	|- Atoms
5	1	cv	|- k
6	5 4	cfv	|- ( Atoms ` k )
7	6	cpw	|- ~P ( Atoms ` k )
8		vy	|- y
9		cpsubsp	|- PSubSp
10	5 9	cfv	|- ( PSubSp ` k )
11	3	cv	|- x
12	8	cv	|- y
13	11 12	wss	|- x C_ y
14	13 8 10	crab	|- { y e. ( PSubSp ` k ) | x C_ y }
15	14	cint	|- |^| { y e. ( PSubSp ` k ) | x C_ y }
16	3 7 15	cmpt	|- ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } )
17	1 2 16	cmpt	|- ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )
18	0 17	wceq	|- PCl = ( k e. _V |-> ( x e. ~P ( Atoms ` k ) |-> |^| { y e. ( PSubSp ` k ) | x C_ y } ) )