Definition df-psubclN 35221

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.)

Assertion

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

Distinct variable group:   k, s

Detailed syntax breakdown of Definition df-psubclN

Step	Hyp	Ref	Expression
1		cpscN 35220	. 2 class PSubCl
2		vk	. . 3 setvar k
3		cvv 3200	. . 3 class _V
4		vs	. . . . . . 7 setvar s
5	4	cv 1482	. . . . . 6 class s
6	2	cv 1482	. . . . . . 7 class k
7		catm 34550	. . . . . . 7 class Atoms
8	6, 7	cfv 5888	. . . . . 6 class ( Atoms ` k )
9	5, 8	wss 3574	. . . . 5 wff s C_ ( Atoms ` k )
10		cpolN 35188	. . . . . . . . 9 class _|_P
11	6, 10	cfv 5888	. . . . . . . 8 class ( _|_P ` k )
12	5, 11	cfv 5888	. . . . . . 7 class ( ( _|_P ` k ) ` s )
13	12, 11	cfv 5888	. . . . . 6 class ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) )
14	13, 5	wceq 1483	. . . . 5 wff ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s
15	9, 14	wa 384	. . . 4 wff ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s )
16	15, 4	cab 2608	. . 3 class { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) }
17	2, 3, 16	cmpt 4729	. 2 class ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )
18	1, 17	wceq 1483	1 wff PSubCl = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )

This definition is referenced by:  psubclsetN  35222