Definition df-psubclN

Description: Define set of all closed projective subspaces, which are those sets of atoms that equal their double polarity. Based on definition in Holland95 p. 223. (Contributed by NM, 23-Jan-2012)

	Ref	Expression
Assertion	df-psubclN	|- PSubCl = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpscN	|- PSubCl
1		vk	|- k
2		cvv	|- _V
3		vs	|- s
4	3	cv	|- s
5		catm	|- Atoms
6	1	cv	|- k
7	6 5	cfv	|- ( Atoms ` k )
8	4 7	wss	|- s C_ ( Atoms ` k )
9		cpolN	|- _|_P
10	6 9	cfv	|- ( _|_P ` k )
11	4 10	cfv	|- ( ( _|_P ` k ) ` s )
12	11 10	cfv	|- ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) )
13	12 4	wceq	|- ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s
14	8 13	wa	|- ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s )
15	14 3	cab	|- { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) }
16	1 2 15	cmpt	|- ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )
17	0 16	wceq	|- PSubCl = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )